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

Theorem exp32 630
 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 450 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 452 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  exp44  640  exp45  641  expr  642  anassrs  679  an13s  844  3impb  1258  reusv2lem2OLD  4861  wereu  5100  f0rn0  6077  funfvima3  6480  isomin  6572  isoini  6573  ovg  6784  elovmpt3rab1  6878  onint  6980  peano5  7074  tfrlem11  7469  tz7.48lem  7521  oalimcl  7625  oaass  7626  resixpfo  7931  fundmen  8015  php3  8131  ssfi  8165  fodomfi  8224  marypha1lem  8324  card2inf  8445  ixpiunwdom  8481  cantnflt  8554  cnfcom  8582  dfac3  8929  dfac5lem5  8935  dfac5  8936  cfcoflem  9079  fin1a2s  9221  zorn2lem4  9306  zorn2lem7  9309  fpwwe2lem12  9448  wunfi  9528  grur1a  9626  addcanpi  9706  mulcanpi  9707  distrlem1pr  9832  ltaddpr  9841  ltexprlem1  9843  ltexprlem6  9848  ltexprlem7  9849  prodgt0  10853  mulgt1  10867  uzwo  11736  xmulasslem  12100  xlemul1a  12103  faclbnd  13060  swrdccatin12lem2a  13466  swrdccat3  13473  swrdccat  13474  cshwidxmod  13530  s3iunsndisj  13688  dvdsaddre2b  15010  divgcdcoprm0  15360  cncongr2  15363  infpnlem1  15595  isacs4lem  17149  gsmsymgrfixlem1  17828  gsmsymgrfix  17829  dmdprdsplit2lem  18425  pgpfac1  18460  pgpfac  18464  lssssr  18934  islmhm2  19019  lspdisj  19106  cygznlem2a  19897  lindfmm  20147  scmataddcl  20303  scmatsubcl  20304  scmatmulcl  20305  cayhamlem3  20673  cayleyhamilton1  20678  neindisj  20902  cnpnei  21049  t0dist  21110  ordthauslem  21168  uncmp  21187  fiuncmp  21188  iunconnlem  21211  fbasrn  21669  rnelfmlem  21737  rnelfm  21738  fmfnfmlem2  21740  fmfnfmlem4  21742  fclscf  21810  alexsubALTlem3  21834  alexsubALTlem4  21835  alexsubALT  21836  reconn  22612  fsumcn  22654  ovolfiniun  23250  dyadmax  23347  dyadmbllem  23348  dvmptfsum  23719  dvlip2  23739  dvivthlem1  23752  dvcnvrelem1  23761  ply1divex  23877  fta1g  23908  plydivex  24033  fta1  24044  mulcxp  24412  zabsle1  25002  lgsquad2lem2  25091  2lgsoddprm  25122  pntlem3  25279  brbtwn  25760  brcgr  25761  brbtwn2  25766  axeuclid  25824  finsumvtxdg2size  26427  uhgrwkspthlem2  26631  crctcshwlkn0  26694  wwlksnred  26768  wwlksnextinj  26775  wspthsnwspthsnon  26792  umgr2wlk  26826  elwwlks2  26842  clwlkclwwlklem2a  26880  wwlksext2clwwlk  26904  eupth2lems  27078  clwwlkextfrlem1  27183  frgrregord013  27223  grpoidinvlem3  27330  shorth  28124  pjhthmo  28131  pjpjpre  28248  elspansn5  28403  lnopmi  28829  adjlnop  28915  leopmul2i  28964  stlesi  29070  ssmd2  29141  dmdsl3  29144  mdexchi  29164  cvexchlem  29197  atcv1  29209  atcvatlem  29214  atabsi  29230  mdsymlem2  29233  mdsymlem5  29236  sumdmdii  29244  sumdmdlem  29247  sumdmdlem2  29248  dya2iocnrect  30317  bnj571  30950  pconnconn  31187  iccllysconn  31206  trpredmintr  31705  poseq  31724  nodenselem8  31815  nocvxmin  31868  cgrextend  32090  btwnexch2  32105  colineardim1  32143  lineext  32158  btwnconn1lem13  32181  btwnconn1lem14  32182  seglecgr12im  32192  outsideofeq  32212  outsideofeu  32213  nn0prpwlem  32292  neibastop2lem  32330  tailfb  32347  nndivsub  32431  ee7.2aOLD  32435  poimirlem31  33411  heicant  33415  filbcmb  33506  prdsbnd2  33565  heibor  33591  rngoisocnv  33751  ax12eq  34045  ax12el  34046  pmodlem2  34952  cdleme22b  35448  cdleme32d  35551  cdleme32f  35553  trlord  35676  cdlemj2  35929  cdlemk38  36022  cdlemk19x  36050  dihord2pre  36333  mzpcompact2lem  37133  pellfundex  37269  acongsym  37362  pwssplit4  37478  pwslnm  37483  relexpmulg  37821  stoweidlem17  39997  iccpartigtl  41123  pfxccat3  41191  fmtnofac2lem  41245  2pwp1prmfmtno  41269  lighneallem4  41292  bgoldbtbndlem2  41459  bgoldbtbndlem3  41460  bgoldbtbnd  41462  lmod0rng  41633  2zrngamgm  41704
 Copyright terms: Public domain W3C validator