MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imp32 Structured version   Visualization version   GIF version

Theorem imp32 448
Description: An importation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
impd.1 (𝜑 → (𝜓 → (𝜒𝜃)))
Assertion
Ref Expression
imp32 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)

Proof of Theorem imp32
StepHypRef Expression
1 impd.1 . . 3 (𝜑 → (𝜓 → (𝜒𝜃)))
21impd 446 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32imp 444 1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 197  df-an 385
This theorem is referenced by:  imp42  619  impr  648  anasss  680  an13s  862  3expb  1285  reuss2  3940  reupick  3944  po2nr  5077  tz7.7  5787  ordtr2  5806  fvmptt  6339  fliftfund  6603  isomin  6627  f1ocnv2d  6928  onint  7037  tz7.48lem  7581  oalimcl  7685  oaass  7686  omass  7705  omabs  7772  finsschain  8314  infxpenlem  8874  axcc3  9298  zorn2lem7  9362  addclpi  9752  addnidpi  9761  genpnnp  9865  genpnmax  9867  mulclprlem  9879  dedekindle  10239  prodgt0  10906  ltsubrp  11904  ltaddrp  11905  swrdccatin1  13529  swrdccat3  13538  sumeven  15157  sumodd  15158  lcmfunsnlem2lem1  15398  divgcdcoprm0  15426  infpnlem1  15661  prmgaplem4  15805  iscatd  16381  imasmnd2  17374  imasgrp2  17577  imasring  18665  mplcoe5lem  19515  dmatmul  20351  scmatmulcl  20372  scmatsgrp1  20376  smatvscl  20378  cpmatacl  20569  cpmatmcllem  20571  0ntr  20923  clsndisj  20927  innei  20977  islpi  21001  tgcnp  21105  haust1  21204  alexsublem  21895  alexsubb  21897  isxmetd  22178  2lgslem1a1  25159  axcontlem4  25892  ewlkle  26557  wlkwwlksur  26851  clwwlkf  27010  clwwlknonwwlknonb  27080  clwwlknonwwlknonbOLD  27081  uhgr3cyclexlem  27159  numclwwlk2lem1lemOLD  27325  numclwlk1lem2foa  27344  grpoidinvlem3  27488  elspansn5  28561  5oalem6  28646  mdi  29282  dmdi  29289  dmdsl3  29302  atom1d  29340  cvexchlem  29355  atcvatlem  29372  chirredlem3  29379  mdsymlem5  29394  f1o3d  29559  bnj570  31101  dfon2lem6  31817  frmin  31867  soseq  31879  nodense  31967  broutsideof2  32354  outsideoftr  32361  outsideofeq  32362  elicc3  32436  nn0prpwlem  32442  nndivsub  32581  bddiblnc  33610  ftc1anc  33623  cntotbnd  33725  heiborlem6  33745  pridlc3  34002  leat2  34899  cvrexchlem  35023  cvratlem  35025  3dim2  35072  ps-2  35082  lncvrelatN  35385  osumcllem11N  35570  iccpartgt  41688  pfxccat3  41751  odz2prm2pw  41800  bgoldbachlt  42026  tgblthelfgott  42028  tgoldbach  42030  bgoldbachltOLD  42032  tgblthelfgottOLD  42034  tgoldbachOLD  42037  funcrngcsetcALT  42324
  Copyright terms: Public domain W3C validator