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

Theorem exp32 421
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 413 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
32expd 416 1 (𝜑 → (𝜓 → (𝜒𝜃)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  exp44  438  exp45  439  expr  457  anassrs  468  an13s  647  3impb  1107  wereu  5545  f0rn0  6558  funfvima3  6989  isomin  7079  isoini  7080  ovg  7302  elovmpt3rab1  7394  onint  7498  peano5  7593  tfrlem11  8015  tz7.48lem  8068  oalimcl  8176  oaass  8177  resixpfo  8489  fundmen  8572  php3  8692  ssfi  8727  fodomfi  8786  marypha1lem  8886  card2inf  9008  ixpiunwdom  9044  cantnflt  9124  cnfcom  9152  dfac3  9536  dfac5lem5  9542  dfac5  9543  cfcoflem  9683  fin1a2s  9825  zorn2lem4  9910  zorn2lem7  9913  fpwwe2lem12  10052  wunfi  10132  grur1a  10230  addcanpi  10310  mulcanpi  10311  distrlem1pr  10436  ltaddpr  10445  ltexprlem1  10447  ltexprlem6  10452  ltexprlem7  10453  prodgt0  11476  mulgt1  11488  uzwo  12300  xmulasslem  12668  xlemul1a  12671  faclbnd  13640  swrdwrdsymb  14014  pfxccatin12lem2a  14079  pfxccat3  14086  swrdccat  14087  cshwidxmod  14155  s3iunsndisj  14318  dvdsaddre2b  15647  divgcdcoprm0  15999  cncongr2  16002  infpnlem1  16236  isacs4lem  17768  cycsubm  18285  gsmsymgrfixlem1  18486  gsmsymgrfix  18487  dmdprdsplit2lem  19098  pgpfac1  19133  pgpfac  19137  lssssr  19656  islmhm2  19741  lspdisj  19828  cygznlem2a  20644  lindfmm  20901  scmataddcl  21055  scmatsubcl  21056  scmatmulcl  21057  cpmatacl  21254  cayhamlem3  21425  cayleyhamilton1  21430  neindisj  21655  cnpnei  21802  t0dist  21863  ordthauslem  21921  uncmp  21941  fiuncmp  21942  iunconnlem  21965  fbasrn  22422  rnelfmlem  22490  rnelfm  22491  fmfnfmlem2  22493  fmfnfmlem4  22495  fclscf  22563  alexsubALTlem3  22587  alexsubALTlem4  22588  alexsubALT  22589  reconn  23365  fsumcn  23407  ovolfiniun  24031  dyadmax  24128  dyadmbllem  24129  dvmptfsum  24501  dvlip2  24521  dvivthlem1  24534  dvcnvrelem1  24543  ply1divex  24659  fta1g  24690  plydivex  24815  fta1  24826  mulcxp  25195  zabsle1  25800  lgsquad2lem2  25889  2lgsoddprm  25920  pntlem3  26113  brbtwn  26613  brcgr  26614  brbtwn2  26619  axeuclid  26677  finsumvtxdg2size  27260  uhgrwkspthlem2  27463  crctcshwlkn0  27527  wwlksnred  27598  wwlksnextinj  27605  umgr2wlk  27656  elwwlks2  27673  clwlkclwwlklem2a  27704  clwlkclwwlkf1lem3  27712  eupth2lems  27945  numclwwlk2lem1lem  28049  frgrregord013  28102  grpoidinvlem3  28211  shorth  29000  pjhthmo  29007  pjpjpre  29124  elspansn5  29279  lnopmi  29705  adjlnop  29791  leopmul2i  29840  stlesi  29946  ssmd2  30017  dmdsl3  30020  mdexchi  30040  cvexchlem  30073  atcv1  30085  atcvatlem  30090  atabsi  30106  mdsymlem2  30109  mdsymlem5  30112  sumdmdii  30120  sumdmdlem  30123  sumdmdlem2  30124  dya2iocnrect  31439  bnj571  32078  pconnconn  32376  iccllysconn  32395  satffunlem2lem1  32549  trpredmintr  32968  poseq  32993  nodenselem8  33093  nocvxmin  33146  cgrextend  33367  btwnexch2  33382  colineardim1  33420  lineext  33435  btwnconn1lem13  33458  btwnconn1lem14  33459  seglecgr12im  33469  outsideofeq  33489  outsideofeu  33490  nn0prpwlem  33568  neibastop2lem  33606  tailfb  33623  nndivsub  33703  ee7.2aOLD  33707  fvineqsneu  34575  poimirlem31  34805  heicant  34809  filbcmb  34898  prdsbnd2  34956  heibor  34982  rngoisocnv  35142  ax12eq  35959  ax12el  35960  pmodlem2  36865  cdleme22b  37359  cdleme32d  37462  cdleme32f  37464  trlord  37587  cdlemj2  37840  cdlemk38  37933  cdlemk19x  37961  dihord2pre  38243  mzpcompact2lem  39228  pellfundex  39363  acongsym  39453  pwssplit4  39569  pwslnm  39574  relexpmulg  39935  stoweidlem17  42183  2reu8i  43193  iccpartigtl  43430  paireqne  43520  fmtnofac2lem  43577  2pwp1prmfmtno  43599  lighneallem4  43622  bgoldbtbndlem2  43818  bgoldbtbndlem3  43819  bgoldbtbnd  43821  lmod0rng  44037  2zrngamgm  44108
  Copyright terms: Public domain W3C validator