Theorem exp32 413

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 403	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 406	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  exp44  430  exp45  431  expr  450  anassrs  461  an13s  641  3impb  1147  wereu  5342  f0rn0  6331  funfvima3  6756  isomin  6847  isoini  6848  ovg  7064  elovmpt3rab1  7158  onint  7261  peano5  7355  tfrlem11  7755  tz7.48lem  7807  oalimcl  7912  oaass  7913  resixpfo  8219  fundmen  8302  php3  8421  ssfi  8455  fodomfi  8514  marypha1lem  8614  card2inf  8736  ixpiunwdom  8772  cantnflt  8853  cnfcom  8881  dfac3  9264  dfac5lem5  9270  dfac5  9271  cfcoflem  9416  fin1a2s  9558  zorn2lem4  9643  zorn2lem7  9646  fpwwe2lem12  9785  wunfi  9865  grur1a  9963  addcanpi  10043  mulcanpi  10044  distrlem1pr  10169  ltaddpr  10178  ltexprlem1  10180  ltexprlem6  10185  ltexprlem7  10186  prodgt0  11205  mulgt1  11219  uzwo  12041  xmulasslem  12410  xlemul1a  12413  faclbnd  13377  swrdwrdsymb  13743  swrdccatin12lem2a  13830  pfxccat3  13840  swrdccat3OLD  13841  swrdccat  13842  swrdccatOLD  13843  cshwidxmod  13931  s3iunsndisj  14093  dvdsaddre2b  15413  divgcdcoprm0  15758  cncongr2  15761  infpnlem1  15992  isacs4lem  17528  gsmsymgrfixlem1  18204  gsmsymgrfix  18205  dmdprdsplit2lem  18805  pgpfac1  18840  pgpfac  18844  lssssr  19318  lssssrOLD  19319  islmhm2  19404  lspdisj  19491  cygznlem2a  20282  lindfmm  20540  scmataddcl  20697  scmatsubcl  20698  scmatmulcl  20699  cayhamlem3  21069  cayleyhamilton1  21074  neindisj  21299  cnpnei  21446  t0dist  21507  ordthauslem  21565  uncmp  21584  fiuncmp  21585  iunconnlem  21608  fbasrn  22065  rnelfmlem  22133  rnelfm  22134  fmfnfmlem2  22136  fmfnfmlem4  22138  fclscf  22206  alexsubALTlem3  22230  alexsubALTlem4  22231  alexsubALT  22232  reconn  23008  fsumcn  23050  ovolfiniun  23674  dyadmax  23771  dyadmbllem  23772  dvmptfsum  24144  dvlip2  24164  dvivthlem1  24177  dvcnvrelem1  24186  ply1divex  24302  fta1g  24333  plydivex  24458  fta1  24469  mulcxp  24837  zabsle1  25441  lgsquad2lem2  25530  2lgsoddprm  25561  pntlem3  25718  brbtwn  26205  brcgr  26206  brbtwn2  26211  axeuclid  26269  finsumvtxdg2size  26855  uhgrwkspthlem2  27063  crctcshwlkn0  27127  wwlksnred  27209  wwlksnredOLD  27210  wwlksnextinj  27220  wwlksnextinjOLD  27225  umgr2wlk  27285  elwwlks2  27302  clwlkclwwlklem2a  27334  clwlkclwwlkf1lem3  27345  clwlkclwwlkf1lem3OLD  27346  eupth2lems  27611  numclwwlk2lem1lem  27719  frgrregord013  27806  grpoidinvlem3  27912  shorth  28705  pjhthmo  28712  pjpjpre  28829  elspansn5  28984  lnopmi  29410  adjlnop  29496  leopmul2i  29545  stlesi  29651  ssmd2  29722  dmdsl3  29725  mdexchi  29745  cvexchlem  29778  atcv1  29790  atcvatlem  29795  atabsi  29811  mdsymlem2  29814  mdsymlem5  29817  sumdmdii  29825  sumdmdlem  29828  sumdmdlem2  29829  dya2iocnrect  30884  bnj571  31518  pconnconn  31755  iccllysconn  31774  trpredmintr  32264  poseq  32287  nodenselem8  32375  nocvxmin  32428  cgrextend  32649  btwnexch2  32664  colineardim1  32702  lineext  32717  btwnconn1lem13  32740  btwnconn1lem14  32741  seglecgr12im  32751  outsideofeq  32771  outsideofeu  32772  nn0prpwlem  32850  neibastop2lem  32888  tailfb  32905  nndivsub  32984  ee7.2aOLD  32988  poimirlem31  33983  heicant  33987  filbcmb  34077  prdsbnd2  34135  heibor  34161  rngoisocnv  34321  ax12eq  35015  ax12el  35016  pmodlem2  35921  cdleme22b  36415  cdleme32d  36518  cdleme32f  36520  trlord  36643  cdlemj2  36896  cdlemk38  36989  cdlemk19x  37017  dihord2pre  37299  mzpcompact2lem  38157  pellfundex  38293  acongsym  38385  pwssplit4  38501  pwslnm  38506  relexpmulg  38842  stoweidlem17  41026  iccpartigtl  42245  paireqne  42279  fmtnofac2lem  42328  2pwp1prmfmtno  42352  lighneallem4  42375  bgoldbtbndlem2  42542  bgoldbtbndlem3  42543  bgoldbtbnd  42545  lmod0rng  42733  2zrngamgm  42804