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  651  3impb  1115  wereu  5681  f0rn0  6793  funfvima3  7256  isomin  7357  isoini  7358  ovg  7598  elovmpt3rab1  7693  onint  7810  peano5  7915  poseq  8183  tfrlem11  8428  tz7.48lem  8481  oalimcl  8598  oaass  8599  resixpfo  8976  fundmen  9071  ssfiALT  9214  php3  9249  php3OLD  9261  fodomfi  9350  fodomfiOLD  9370  marypha1lem  9473  card2inf  9595  ixpiunwdom  9630  cantnflt  9712  cnfcom  9740  dfac3  10161  dfac5lem5  10167  dfac5  10169  cfcoflem  10312  fin1a2s  10454  zorn2lem4  10539  zorn2lem7  10542  fpwwe2lem11  10681  wunfi  10761  grur1a  10859  addcanpi  10939  mulcanpi  10940  distrlem1pr  11065  ltaddpr  11074  ltexprlem1  11076  ltexprlem6  11081  ltexprlem7  11082  prodgt0  12114  mulgt1OLD  12126  uzwo  12953  xmulasslem  13327  xlemul1a  13330  faclbnd  14329  swrdwrdsymb  14700  pfxccatin12lem2a  14765  pfxccat3  14772  swrdccat  14773  cshwidxmod  14841  s3iunsndisj  15007  dvdsaddre2b  16344  divgcdcoprm0  16702  cncongr2  16705  infpnlem1  16948  isacs4lem  18589  cycsubm  19220  gsmsymgrfixlem1  19445  gsmsymgrfix  19446  imasabl  19894  dmdprdsplit2lem  20065  pgpfac1  20100  pgpfac  20104  lssssr  20952  islmhm2  21037  lspdisj  21127  pzriprnglem5  21496  pzriprnglem8  21499  cygznlem2a  21586  lindfmm  21847  scmataddcl  22522  scmatsubcl  22523  scmatmulcl  22524  cpmatacl  22722  cayhamlem3  22893  cayleyhamilton1  22898  neindisj  23125  cnpnei  23272  t0dist  23333  ordthauslem  23391  uncmp  23411  fiuncmp  23412  iunconnlem  23435  fbasrn  23892  rnelfmlem  23960  rnelfm  23961  fmfnfmlem2  23963  fmfnfmlem4  23965  fclscf  24033  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  reconn  24850  fsumcn  24894  ovolfiniun  25536  dyadmax  25633  dyadmbllem  25634  dvmptfsum  26013  dvlip2  26034  dvivthlem1  26047  dvcnvrelem1  26056  ply1divex  26176  fta1g  26209  plydivex  26339  fta1  26350  mulcxp  26727  zabsle1  27340  lgsquad2lem2  27429  2lgsoddprm  27460  pntlem3  27653  nodenselem8  27736  nocvxmin  27823  precsexlem11  28241  om2noseqrdg  28310  brbtwn  28914  brcgr  28915  brbtwn2  28920  axeuclid  28978  finsumvtxdg2size  29568  uhgrwkspthlem2  29774  crctcshwlkn0  29841  wwlksnred  29912  wwlksnextinj  29919  umgr2wlk  29969  elwwlks2  29986  clwlkclwwlklem2a  30017  clwlkclwwlkf1lem3  30025  eupth2lems  30257  numclwwlk2lem1lem  30361  frgrregord013  30414  grpoidinvlem3  30525  shorth  31314  pjhthmo  31321  pjpjpre  31438  elspansn5  31593  lnopmi  32019  adjlnop  32105  leopmul2i  32154  stlesi  32260  ssmd2  32331  dmdsl3  32334  mdexchi  32354  cvexchlem  32387  atcv1  32399  atcvatlem  32404  atabsi  32420  mdsymlem2  32423  mdsymlem5  32426  sumdmdii  32434  sumdmdlem  32437  sumdmdlem2  32438  dya2iocnrect  34283  bnj571  34920  pconnconn  35236  iccllysconn  35255  satffunlem2lem1  35409  cgrextend  36009  btwnexch2  36024  colineardim1  36062  lineext  36077  btwnconn1lem13  36100  btwnconn1lem14  36101  seglecgr12im  36111  outsideofeq  36131  outsideofeu  36132  nn0prpwlem  36323  neibastop2lem  36361  tailfb  36378  nndivsub  36458  ee7.2aOLD  36462  fvineqsneu  37412  poimirlem31  37658  heicant  37662  filbcmb  37747  prdsbnd2  37802  heibor  37828  rngoisocnv  37988  ax12eq  38942  ax12el  38943  pmodlem2  39849  cdleme22b  40343  cdleme32d  40446  cdleme32f  40448  trlord  40571  cdlemj2  40824  cdlemk38  40917  cdlemk19x  40945  dihord2pre  41227  fsuppind  42600  mzpcompact2lem  42762  pellfundex  42897  acongsym  42988  pwssplit4  43101  pwslnm  43106  cantnfresb  43337  relexpmulg  43723  relpmin  44973  stoweidlem17  46032  2reu8i  47125  imasetpreimafvbijlemf1  47391  iccpartigtl  47410  paireqne  47498  fmtnofac2lem  47555  2pwp1prmfmtno  47577  lighneallem4  47597  bgoldbtbndlem2  47793  bgoldbtbndlem3  47794  bgoldbtbnd  47796  isuspgrimlem  47874  grimco  47880  cycl3grtri  47914  isubgr3stgrlem6  47938  lmod0rng  48145  2zrngamgm  48161