Theorem exp32 425

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  exp44  442  exp45  443  expr  461  anassrs  472  an13s  663  3impb  1130  wereu  5648  f0rn0  6753  funfvima3  7224  dff14i  7247  isomin  7325  isoini  7326  ovg  7565  elovmpt3rab1  7660  onint  7777  peano5  7878  poseq  8142  tfrlem11  8363  tz7.48lem  8416  oalimcl  8533  oaass  8534  resixpfo  8922  fundmen  9016  ssfiALT  9146  php3  9181  fodomfi  9260  marypha1lem  9381  card2inf  9505  ixpiunwdom  9540  cantnflt  9629  cnfcom  9657  dfac3  10093  dfac5lem5  10099  dfac5  10100  cfcoflem  10244  fin1a2s  10386  zorn2lem4  10471  zorn2lem7  10474  fpwwe2lem11  10614  wunfi  10694  grur1a  10792  addcanpi  10872  mulcanpi  10873  distrlem1pr  10998  ltaddpr  11007  ltexprlem1  11009  ltexprlem6  11014  ltexprlem7  11015  prodgt0  12053  uzwo  12926  xmulasslem  13302  xlemul1a  13305  faclbnd  14317  swrdwrdsymb  14690  pfxccatin12lem2a  14754  pfxccat3  14761  swrdccat  14762  cshwidxmod  14830  s3iunsndisj  14995  dvdsaddre2b  16355  divgcdcoprm0  16713  cncongr2  16716  infpnlem1  16960  isacs4lem  18590  cycsubm  19264  gsmsymgrfixlem1  19488  gsmsymgrfix  19489  imasabl  19937  dmdprdsplit2lem  20108  pgpfac1  20143  pgpfac  20147  lssssr  21044  islmhm2  21128  lspdisj  21218  pzriprnglem5  21595  pzriprnglem8  21598  cygznlem2a  21677  lindfmm  21937  scmataddcl  22634  scmatsubcl  22635  scmatmulcl  22636  cpmatacl  22834  cayhamlem3  23005  cayleyhamilton1  23010  neindisj  23235  cnpnei  23382  t0dist  23443  ordthauslem  23501  uncmp  23521  fiuncmp  23522  iunconnlem  23545  fbasrn  24002  rnelfmlem  24070  rnelfm  24071  fmfnfmlem2  24073  fmfnfmlem4  24075  fclscf  24143  alexsubALTlem3  24167  alexsubALTlem4  24168  alexsubALT  24169  reconn  24947  fsumcn  24990  ovolfiniun  25621  dyadmax  25718  dyadmbllem  25719  dvmptfsum  26095  dvlip2  26115  dvivthlem1  26128  dvcnvrelem1  26137  ply1divex  26255  fta1g  26288  plydivex  26419  fta1  26430  mulcxp  26808  zabsle1  27418  lgsquad2lem2  27507  2lgsoddprm  27538  pntlem3  27731  nodenselem8  27813  nocvxmin  27906  precsexlem11  28368  om2noseqrdg  28455  expadds  28586  brbtwn  29158  brcgr  29159  brbtwn2  29164  axeuclid  29222  finsumvtxdg2size  29809  uhgrwkspthlem2  30012  crctcshwlkn0  30079  wwlksnred  30150  wwlksnextinj  30157  umgr2wlk  30207  elwwlks2  30227  clwlkclwwlklem2a  30258  clwlkclwwlkf1lem3  30266  eupth2lems  30498  numclwwlk2lem1lem  30602  frgrregord013  30655  grpoidinvlem3  30767  shorth  31556  pjhthmo  31563  pjpjpre  31680  elspansn5  31835  lnopmi  32261  adjlnop  32347  leopmul2i  32396  stlesi  32502  ssmd2  32573  dmdsl3  32576  mdexchi  32596  cvexchlem  32629  atcv1  32641  atcvatlem  32646  atabsi  32662  mdsymlem2  32665  mdsymlem5  32668  sumdmdii  32676  sumdmdlem  32679  sumdmdlem2  32680  dya2iocnrect  34588  bnj571  35211  pconnconn  35594  iccllysconn  35613  satffunlem2lem1  35767  cgrextend  36371  btwnexch2  36386  colineardim1  36424  lineext  36439  btwnconn1lem13  36462  btwnconn1lem14  36463  seglecgr12im  36473  outsideofeq  36493  outsideofeu  36494  nn0prpwlem  36695  neibastop2lem  36733  tailfb  36750  nndivsub  36830  ee7.2aOLD  36834  fvineqsneu  37917  poimirlem31  38162  heicant  38166  filbcmb  38251  prdsbnd2  38306  heibor  38332  rngoisocnv  38492  ax12eq  39577  ax12el  39578  pmodlem2  40483  cdleme22b  40977  cdleme32d  41080  cdleme32f  41082  trlord  41205  cdlemj2  41458  cdlemk38  41551  cdlemk19x  41579  dihord2pre  41861  fsuppind  43184  mzpcompact2lem  43344  pellfundex  43475  acongsym  43565  pwssplit4  43678  pwslnm  43683  cantnfresb  43913  relexpmulg  44298  relpmin  45526  stoweidlem17  46589  2reu8i  47705  imasetpreimafvbijlemf1  48008  iccpartigtl  48027  paireqne  48115  fmtnofac2lem  48175  2pwp1prmfmtno  48197  lighneallem4  48217  bgoldbtbndlem2  48426  bgoldbtbndlem3  48427  bgoldbtbnd  48429  grimco  48509  isuspgrimlem  48515  cycl3grtri  48567  isubgr3stgrlem6  48591  lmod0rng  48849  2zrngamgm  48865