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

Theorem exp32 423
Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)
Hypothesis
Ref Expression
exp32.1 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
exp32 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem exp32
StepHypRef Expression
1 exp32.1 . . 3 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
21ex 415 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 418 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 398
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 209  df-an 399
This theorem is referenced by:  exp44  440  exp45  441  expr  459  anassrs  470  an13s  649  3impb  1111  wereu  5550  f0rn0  6563  funfvima3  6997  isomin  7089  isoini  7090  ovg  7312  elovmpt3rab1  7404  onint  7509  peano5  7604  tfrlem11  8023  tz7.48lem  8076  oalimcl  8185  oaass  8186  resixpfo  8499  fundmen  8582  php3  8702  ssfi  8737  fodomfi  8796  marypha1lem  8896  card2inf  9018  ixpiunwdom  9054  cantnflt  9134  cnfcom  9162  dfac3  9546  dfac5lem5  9552  dfac5  9553  cfcoflem  9693  fin1a2s  9835  zorn2lem4  9920  zorn2lem7  9923  fpwwe2lem12  10062  wunfi  10142  grur1a  10240  addcanpi  10320  mulcanpi  10321  distrlem1pr  10446  ltaddpr  10455  ltexprlem1  10457  ltexprlem6  10462  ltexprlem7  10463  prodgt0  11486  mulgt1  11498  uzwo  12310  xmulasslem  12677  xlemul1a  12680  faclbnd  13649  swrdwrdsymb  14023  pfxccatin12lem2a  14088  pfxccat3  14095  swrdccat  14096  cshwidxmod  14164  s3iunsndisj  14327  dvdsaddre2b  15656  divgcdcoprm0  16008  cncongr2  16011  infpnlem1  16245  isacs4lem  17777  cycsubm  18344  gsmsymgrfixlem1  18554  gsmsymgrfix  18555  dmdprdsplit2lem  19166  pgpfac1  19201  pgpfac  19205  lssssr  19724  islmhm2  19809  lspdisj  19896  cygznlem2a  20713  lindfmm  20970  scmataddcl  21124  scmatsubcl  21125  scmatmulcl  21126  cpmatacl  21323  cayhamlem3  21494  cayleyhamilton1  21499  neindisj  21724  cnpnei  21871  t0dist  21932  ordthauslem  21990  uncmp  22010  fiuncmp  22011  iunconnlem  22034  fbasrn  22491  rnelfmlem  22559  rnelfm  22560  fmfnfmlem2  22562  fmfnfmlem4  22564  fclscf  22632  alexsubALTlem3  22656  alexsubALTlem4  22657  alexsubALT  22658  reconn  23435  fsumcn  23477  ovolfiniun  24101  dyadmax  24198  dyadmbllem  24199  dvmptfsum  24571  dvlip2  24591  dvivthlem1  24604  dvcnvrelem1  24613  ply1divex  24729  fta1g  24760  plydivex  24885  fta1  24896  mulcxp  25267  zabsle1  25871  lgsquad2lem2  25960  2lgsoddprm  25991  pntlem3  26184  brbtwn  26684  brcgr  26685  brbtwn2  26690  axeuclid  26748  finsumvtxdg2size  27331  uhgrwkspthlem2  27534  crctcshwlkn0  27598  wwlksnred  27669  wwlksnextinj  27676  umgr2wlk  27727  elwwlks2  27744  clwlkclwwlklem2a  27775  clwlkclwwlkf1lem3  27783  eupth2lems  28016  numclwwlk2lem1lem  28120  frgrregord013  28173  grpoidinvlem3  28282  shorth  29071  pjhthmo  29078  pjpjpre  29195  elspansn5  29350  lnopmi  29776  adjlnop  29862  leopmul2i  29911  stlesi  30017  ssmd2  30088  dmdsl3  30091  mdexchi  30111  cvexchlem  30144  atcv1  30156  atcvatlem  30161  atabsi  30177  mdsymlem2  30180  mdsymlem5  30183  sumdmdii  30191  sumdmdlem  30194  sumdmdlem2  30195  dya2iocnrect  31539  bnj571  32178  pconnconn  32478  iccllysconn  32497  satffunlem2lem1  32651  trpredmintr  33070  poseq  33095  nodenselem8  33195  nocvxmin  33248  cgrextend  33469  btwnexch2  33484  colineardim1  33522  lineext  33537  btwnconn1lem13  33560  btwnconn1lem14  33561  seglecgr12im  33571  outsideofeq  33591  outsideofeu  33592  nn0prpwlem  33670  neibastop2lem  33708  tailfb  33725  nndivsub  33805  ee7.2aOLD  33809  fvineqsneu  34691  poimirlem31  34922  heicant  34926  filbcmb  35014  prdsbnd2  35072  heibor  35098  rngoisocnv  35258  ax12eq  36076  ax12el  36077  pmodlem2  36982  cdleme22b  37476  cdleme32d  37579  cdleme32f  37581  trlord  37704  cdlemj2  37957  cdlemk38  38050  cdlemk19x  38078  dihord2pre  38360  mzpcompact2lem  39346  pellfundex  39481  acongsym  39571  pwssplit4  39687  pwslnm  39692  relexpmulg  40053  stoweidlem17  42301  2reu8i  43311  imasetpreimafvbijlemf1  43563  iccpartigtl  43582  paireqne  43672  fmtnofac2lem  43729  2pwp1prmfmtno  43751  lighneallem4  43774  bgoldbtbndlem2  43970  bgoldbtbndlem3  43971  bgoldbtbnd  43973  lmod0rng  44138  2zrngamgm  44209
  Copyright terms: Public domain W3C validator