Theorem exp32 420

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp32.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
exp32	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	ex 412	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 415	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp44  437  exp45  438  expr  456  anassrs  467  an13s  652  3impb  1115  wereu  5627  f0rn0  6725  funfvima3  7191  dff14i  7214  isomin  7292  isoini  7293  ovg  7532  elovmpt3rab1  7627  onint  7744  peano5  7844  poseq  8108  tfrlem11  8327  tz7.48lem  8380  oalimcl  8495  oaass  8496  resixpfo  8884  fundmen  8978  ssfiALT  9108  php3  9143  fodomfi  9222  fodomfiOLD  9240  marypha1lem  9346  card2inf  9470  ixpiunwdom  9505  cantnflt  9593  cnfcom  9621  dfac3  10043  dfac5lem5  10049  dfac5  10051  cfcoflem  10194  fin1a2s  10336  zorn2lem4  10421  zorn2lem7  10424  fpwwe2lem11  10564  wunfi  10644  grur1a  10742  addcanpi  10822  mulcanpi  10823  distrlem1pr  10948  ltaddpr  10957  ltexprlem1  10959  ltexprlem6  10964  ltexprlem7  10965  prodgt0  12002  mulgt1OLD  12014  uzwo  12861  xmulasslem  13237  xlemul1a  13240  faclbnd  14252  swrdwrdsymb  14625  pfxccatin12lem2a  14689  pfxccat3  14696  swrdccat  14697  cshwidxmod  14765  s3iunsndisj  14930  dvdsaddre2b  16276  divgcdcoprm0  16634  cncongr2  16637  infpnlem1  16881  isacs4lem  18510  cycsubm  19177  gsmsymgrfixlem1  19402  gsmsymgrfix  19403  imasabl  19851  dmdprdsplit2lem  20022  pgpfac1  20057  pgpfac  20061  lssssr  20949  islmhm2  21033  lspdisj  21123  pzriprnglem5  21465  pzriprnglem8  21468  cygznlem2a  21547  lindfmm  21807  scmataddcl  22481  scmatsubcl  22482  scmatmulcl  22483  cpmatacl  22681  cayhamlem3  22852  cayleyhamilton1  22857  neindisj  23082  cnpnei  23229  t0dist  23290  ordthauslem  23348  uncmp  23368  fiuncmp  23369  iunconnlem  23392  fbasrn  23849  rnelfmlem  23917  rnelfm  23918  fmfnfmlem2  23920  fmfnfmlem4  23922  fclscf  23990  alexsubALTlem3  24014  alexsubALTlem4  24015  alexsubALT  24016  reconn  24794  fsumcn  24837  ovolfiniun  25468  dyadmax  25565  dyadmbllem  25566  dvmptfsum  25942  dvlip2  25962  dvivthlem1  25975  dvcnvrelem1  25984  ply1divex  26102  fta1g  26135  plydivex  26263  fta1  26274  mulcxp  26649  zabsle1  27259  lgsquad2lem2  27348  2lgsoddprm  27379  pntlem3  27572  nodenselem8  27655  nocvxmin  27747  precsexlem11  28209  om2noseqrdg  28296  expadds  28427  brbtwn  28968  brcgr  28969  brbtwn2  28974  axeuclid  29032  finsumvtxdg2size  29619  uhgrwkspthlem2  29822  crctcshwlkn0  29889  wwlksnred  29960  wwlksnextinj  29967  umgr2wlk  30017  elwwlks2  30037  clwlkclwwlklem2a  30068  clwlkclwwlkf1lem3  30076  eupth2lems  30308  numclwwlk2lem1lem  30412  frgrregord013  30465  grpoidinvlem3  30577  shorth  31366  pjhthmo  31373  pjpjpre  31490  elspansn5  31645  lnopmi  32071  adjlnop  32157  leopmul2i  32206  stlesi  32312  ssmd2  32383  dmdsl3  32386  mdexchi  32406  cvexchlem  32439  atcv1  32451  atcvatlem  32456  atabsi  32472  mdsymlem2  32475  mdsymlem5  32478  sumdmdii  32486  sumdmdlem  32489  sumdmdlem2  32490  dya2iocnrect  34425  bnj571  35048  pconnconn  35413  iccllysconn  35432  satffunlem2lem1  35586  cgrextend  36190  btwnexch2  36205  colineardim1  36243  lineext  36258  btwnconn1lem13  36281  btwnconn1lem14  36282  seglecgr12im  36292  outsideofeq  36312  outsideofeu  36313  nn0prpwlem  36504  neibastop2lem  36542  tailfb  36559  nndivsub  36639  ee7.2aOLD  36643  fvineqsneu  37727  poimirlem31  37972  heicant  37976  filbcmb  38061  prdsbnd2  38116  heibor  38142  rngoisocnv  38302  ax12eq  39387  ax12el  39388  pmodlem2  40293  cdleme22b  40787  cdleme32d  40890  cdleme32f  40892  trlord  41015  cdlemj2  41268  cdlemk38  41361  cdlemk19x  41389  dihord2pre  41671  fsuppind  43023  mzpcompact2lem  43183  pellfundex  43314  acongsym  43404  pwssplit4  43517  pwslnm  43522  cantnfresb  43752  relexpmulg  44137  relpmin  45379  stoweidlem17  46445  2reu8i  47561  imasetpreimafvbijlemf1  47864  iccpartigtl  47883  paireqne  47971  fmtnofac2lem  48031  2pwp1prmfmtno  48053  lighneallem4  48073  bgoldbtbndlem2  48282  bgoldbtbndlem3  48283  bgoldbtbnd  48285  grimco  48365  isuspgrimlem  48371  cycl3grtri  48423  isubgr3stgrlem6  48447  lmod0rng  48705  2zrngamgm  48721