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  5620  f0rn0  6719  funfvima3  7184  dff14i  7207  isomin  7285  isoini  7286  ovg  7525  elovmpt3rab1  7620  onint  7737  peano5  7837  poseq  8101  tfrlem11  8320  tz7.48lem  8373  oalimcl  8488  oaass  8489  resixpfo  8877  fundmen  8971  ssfiALT  9101  php3  9136  fodomfi  9215  fodomfiOLD  9233  marypha1lem  9339  card2inf  9463  ixpiunwdom  9498  cantnflt  9584  cnfcom  9612  dfac3  10034  dfac5lem5  10040  dfac5  10042  cfcoflem  10185  fin1a2s  10327  zorn2lem4  10412  zorn2lem7  10415  fpwwe2lem11  10555  wunfi  10635  grur1a  10733  addcanpi  10813  mulcanpi  10814  distrlem1pr  10939  ltaddpr  10948  ltexprlem1  10950  ltexprlem6  10955  ltexprlem7  10956  prodgt0  11993  mulgt1OLD  12005  uzwo  12852  xmulasslem  13228  xlemul1a  13231  faclbnd  14243  swrdwrdsymb  14616  pfxccatin12lem2a  14680  pfxccat3  14687  swrdccat  14688  cshwidxmod  14756  s3iunsndisj  14921  dvdsaddre2b  16267  divgcdcoprm0  16625  cncongr2  16628  infpnlem1  16872  isacs4lem  18501  cycsubm  19168  gsmsymgrfixlem1  19393  gsmsymgrfix  19394  imasabl  19842  dmdprdsplit2lem  20013  pgpfac1  20048  pgpfac  20052  lssssr  20940  islmhm2  21025  lspdisj  21115  pzriprnglem5  21475  pzriprnglem8  21478  cygznlem2a  21557  lindfmm  21817  scmataddcl  22491  scmatsubcl  22492  scmatmulcl  22493  cpmatacl  22691  cayhamlem3  22862  cayleyhamilton1  22867  neindisj  23092  cnpnei  23239  t0dist  23300  ordthauslem  23358  uncmp  23378  fiuncmp  23379  iunconnlem  23402  fbasrn  23859  rnelfmlem  23927  rnelfm  23928  fmfnfmlem2  23930  fmfnfmlem4  23932  fclscf  24000  alexsubALTlem3  24024  alexsubALTlem4  24025  alexsubALT  24026  reconn  24804  fsumcn  24847  ovolfiniun  25478  dyadmax  25575  dyadmbllem  25576  dvmptfsum  25952  dvlip2  25972  dvivthlem1  25985  dvcnvrelem1  25994  ply1divex  26112  fta1g  26145  plydivex  26274  fta1  26285  mulcxp  26662  zabsle1  27273  lgsquad2lem2  27362  2lgsoddprm  27393  pntlem3  27586  nodenselem8  27669  nocvxmin  27761  precsexlem11  28223  om2noseqrdg  28310  expadds  28441  brbtwn  28982  brcgr  28983  brbtwn2  28988  axeuclid  29046  finsumvtxdg2size  29634  uhgrwkspthlem2  29837  crctcshwlkn0  29904  wwlksnred  29975  wwlksnextinj  29982  umgr2wlk  30032  elwwlks2  30052  clwlkclwwlklem2a  30083  clwlkclwwlkf1lem3  30091  eupth2lems  30323  numclwwlk2lem1lem  30427  frgrregord013  30480  grpoidinvlem3  30592  shorth  31381  pjhthmo  31388  pjpjpre  31505  elspansn5  31660  lnopmi  32086  adjlnop  32172  leopmul2i  32221  stlesi  32327  ssmd2  32398  dmdsl3  32401  mdexchi  32421  cvexchlem  32454  atcv1  32466  atcvatlem  32471  atabsi  32487  mdsymlem2  32490  mdsymlem5  32493  sumdmdii  32501  sumdmdlem  32504  sumdmdlem2  32505  dya2iocnrect  34441  bnj571  35064  pconnconn  35429  iccllysconn  35448  satffunlem2lem1  35602  cgrextend  36206  btwnexch2  36221  colineardim1  36259  lineext  36274  btwnconn1lem13  36297  btwnconn1lem14  36298  seglecgr12im  36308  outsideofeq  36328  outsideofeu  36329  nn0prpwlem  36520  neibastop2lem  36558  tailfb  36575  nndivsub  36655  ee7.2aOLD  36659  fvineqsneu  37741  poimirlem31  37986  heicant  37990  filbcmb  38075  prdsbnd2  38130  heibor  38156  rngoisocnv  38316  ax12eq  39401  ax12el  39402  pmodlem2  40307  cdleme22b  40801  cdleme32d  40904  cdleme32f  40906  trlord  41029  cdlemj2  41282  cdlemk38  41375  cdlemk19x  41403  dihord2pre  41685  fsuppind  43037  mzpcompact2lem  43197  pellfundex  43332  acongsym  43422  pwssplit4  43535  pwslnm  43540  cantnfresb  43770  relexpmulg  44155  relpmin  45397  stoweidlem17  46463  2reu8i  47573  imasetpreimafvbijlemf1  47876  iccpartigtl  47895  paireqne  47983  fmtnofac2lem  48043  2pwp1prmfmtno  48065  lighneallem4  48085  bgoldbtbndlem2  48294  bgoldbtbndlem3  48295  bgoldbtbnd  48297  grimco  48377  isuspgrimlem  48383  cycl3grtri  48435  isubgr3stgrlem6  48459  lmod0rng  48717  2zrngamgm  48733