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

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

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 206  df-an 397

This theorem is referenced by:  exp44  438  exp45  439  expr  457  anassrs  468  an13s  649  3impb  1115  wereu  5634  f0rn0  6732  funfvima3  7191  isomin  7287  isoini  7288  ovg  7524  elovmpt3rab1  7618  onint  7730  peano5  7835  peano5OLD  7836  poseq  8095  tfrlem11  8339  tz7.48lem  8392  oalimcl  8512  oaass  8513  resixpfo  8881  fundmen  8982  ssfiALT  9125  php3  9163  php3OLD  9175  fodomfi  9276  marypha1lem  9378  card2inf  9500  ixpiunwdom  9535  cantnflt  9617  cnfcom  9645  dfac3  10066  dfac5lem5  10072  dfac5  10073  cfcoflem  10217  fin1a2s  10359  zorn2lem4  10444  zorn2lem7  10447  fpwwe2lem11  10586  wunfi  10666  grur1a  10764  addcanpi  10844  mulcanpi  10845  distrlem1pr  10970  ltaddpr  10979  ltexprlem1  10981  ltexprlem6  10986  ltexprlem7  10987  prodgt0  12011  mulgt1  12023  uzwo  12845  xmulasslem  13214  xlemul1a  13217  faclbnd  14200  swrdwrdsymb  14562  pfxccatin12lem2a  14627  pfxccat3  14634  swrdccat  14635  cshwidxmod  14703  s3iunsndisj  14865  dvdsaddre2b  16200  divgcdcoprm0  16552  cncongr2  16555  infpnlem1  16793  isacs4lem  18447  cycsubm  19009  gsmsymgrfixlem1  19223  gsmsymgrfix  19224  dmdprdsplit2lem  19838  pgpfac1  19873  pgpfac  19877  lssssr  20471  islmhm2  20556  lspdisj  20645  cygznlem2a  21011  lindfmm  21270  scmataddcl  21902  scmatsubcl  21903  scmatmulcl  21904  cpmatacl  22102  cayhamlem3  22273  cayleyhamilton1  22278  neindisj  22505  cnpnei  22652  t0dist  22713  ordthauslem  22771  uncmp  22791  fiuncmp  22792  iunconnlem  22815  fbasrn  23272  rnelfmlem  23340  rnelfm  23341  fmfnfmlem2  23343  fmfnfmlem4  23345  fclscf  23413  alexsubALTlem3  23437  alexsubALTlem4  23438  alexsubALT  23439  reconn  24228  fsumcn  24270  ovolfiniun  24902  dyadmax  24999  dyadmbllem  25000  dvmptfsum  25376  dvlip2  25396  dvivthlem1  25409  dvcnvrelem1  25418  ply1divex  25538  fta1g  25569  plydivex  25694  fta1  25705  mulcxp  26077  zabsle1  26681  lgsquad2lem2  26770  2lgsoddprm  26801  pntlem3  26994  nodenselem8  27076  nocvxmin  27161  brbtwn  27911  brcgr  27912  brbtwn2  27917  axeuclid  27975  finsumvtxdg2size  28561  uhgrwkspthlem2  28765  crctcshwlkn0  28829  wwlksnred  28900  wwlksnextinj  28907  umgr2wlk  28957  elwwlks2  28974  clwlkclwwlklem2a  29005  clwlkclwwlkf1lem3  29013  eupth2lems  29245  numclwwlk2lem1lem  29349  frgrregord013  29402  grpoidinvlem3  29511  shorth  30300  pjhthmo  30307  pjpjpre  30424  elspansn5  30579  lnopmi  31005  adjlnop  31091  leopmul2i  31140  stlesi  31246  ssmd2  31317  dmdsl3  31320  mdexchi  31340  cvexchlem  31373  atcv1  31385  atcvatlem  31390  atabsi  31406  mdsymlem2  31409  mdsymlem5  31412  sumdmdii  31420  sumdmdlem  31423  sumdmdlem2  31424  dya2iocnrect  32970  bnj571  33607  pconnconn  33912  iccllysconn  33931  satffunlem2lem1  34085  cgrextend  34669  btwnexch2  34684  colineardim1  34722  lineext  34737  btwnconn1lem13  34760  btwnconn1lem14  34761  seglecgr12im  34771  outsideofeq  34791  outsideofeu  34792  nn0prpwlem  34870  neibastop2lem  34908  tailfb  34925  nndivsub  35005  ee7.2aOLD  35009  fvineqsneu  35955  poimirlem31  36182  heicant  36186  filbcmb  36272  prdsbnd2  36327  heibor  36353  rngoisocnv  36513  ax12eq  37476  ax12el  37477  pmodlem2  38383  cdleme22b  38877  cdleme32d  38980  cdleme32f  38982  trlord  39105  cdlemj2  39358  cdlemk38  39451  cdlemk19x  39479  dihord2pre  39761  fsuppind  40823  mzpcompact2lem  41132  pellfundex  41267  acongsym  41358  pwssplit4  41474  pwslnm  41479  cantnfresb  41717  relexpmulg  42104  stoweidlem17  44378  2reu8i  45465  imasetpreimafvbijlemf1  45716  iccpartigtl  45735  paireqne  45823  fmtnofac2lem  45880  2pwp1prmfmtno  45902  lighneallem4  45922  bgoldbtbndlem2  46118  bgoldbtbndlem3  46119  bgoldbtbnd  46121  lmod0rng  46286  2zrngamgm  46357