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  1114  wereu  5684  f0rn0  6793  funfvima3  7255  isomin  7356  isoini  7357  ovg  7597  elovmpt3rab1  7692  onint  7809  peano5  7915  poseq  8181  tfrlem11  8426  tz7.48lem  8479  oalimcl  8596  oaass  8597  resixpfo  8974  fundmen  9069  ssfiALT  9212  php3  9246  php3OLD  9258  fodomfi  9347  fodomfiOLD  9367  marypha1lem  9470  card2inf  9592  ixpiunwdom  9627  cantnflt  9709  cnfcom  9737  dfac3  10158  dfac5lem5  10164  dfac5  10166  cfcoflem  10309  fin1a2s  10451  zorn2lem4  10536  zorn2lem7  10539  fpwwe2lem11  10678  wunfi  10758  grur1a  10856  addcanpi  10936  mulcanpi  10937  distrlem1pr  11062  ltaddpr  11071  ltexprlem1  11073  ltexprlem6  11078  ltexprlem7  11079  prodgt0  12111  mulgt1OLD  12123  uzwo  12950  xmulasslem  13323  xlemul1a  13326  faclbnd  14325  swrdwrdsymb  14696  pfxccatin12lem2a  14761  pfxccat3  14768  swrdccat  14769  cshwidxmod  14837  s3iunsndisj  15003  dvdsaddre2b  16340  divgcdcoprm0  16698  cncongr2  16701  infpnlem1  16943  isacs4lem  18601  cycsubm  19232  gsmsymgrfixlem1  19459  gsmsymgrfix  19460  imasabl  19908  dmdprdsplit2lem  20079  pgpfac1  20114  pgpfac  20118  lssssr  20969  islmhm2  21054  lspdisj  21144  pzriprnglem5  21513  pzriprnglem8  21516  cygznlem2a  21603  lindfmm  21864  scmataddcl  22537  scmatsubcl  22538  scmatmulcl  22539  cpmatacl  22737  cayhamlem3  22908  cayleyhamilton1  22913  neindisj  23140  cnpnei  23287  t0dist  23348  ordthauslem  23406  uncmp  23426  fiuncmp  23427  iunconnlem  23450  fbasrn  23907  rnelfmlem  23975  rnelfm  23976  fmfnfmlem2  23978  fmfnfmlem4  23980  fclscf  24048  alexsubALTlem3  24072  alexsubALTlem4  24073  alexsubALT  24074  reconn  24863  fsumcn  24907  ovolfiniun  25549  dyadmax  25646  dyadmbllem  25647  dvmptfsum  26027  dvlip2  26048  dvivthlem1  26061  dvcnvrelem1  26070  ply1divex  26190  fta1g  26223  plydivex  26353  fta1  26364  mulcxp  26741  zabsle1  27354  lgsquad2lem2  27443  2lgsoddprm  27474  pntlem3  27667  nodenselem8  27750  nocvxmin  27837  precsexlem11  28255  om2noseqrdg  28324  brbtwn  28928  brcgr  28929  brbtwn2  28934  axeuclid  28992  finsumvtxdg2size  29582  uhgrwkspthlem2  29786  crctcshwlkn0  29850  wwlksnred  29921  wwlksnextinj  29928  umgr2wlk  29978  elwwlks2  29995  clwlkclwwlklem2a  30026  clwlkclwwlkf1lem3  30034  eupth2lems  30266  numclwwlk2lem1lem  30370  frgrregord013  30423  grpoidinvlem3  30534  shorth  31323  pjhthmo  31330  pjpjpre  31447  elspansn5  31602  lnopmi  32028  adjlnop  32114  leopmul2i  32163  stlesi  32269  ssmd2  32340  dmdsl3  32343  mdexchi  32363  cvexchlem  32396  atcv1  32408  atcvatlem  32413  atabsi  32429  mdsymlem2  32432  mdsymlem5  32435  sumdmdii  32443  sumdmdlem  32446  sumdmdlem2  32447  dya2iocnrect  34262  bnj571  34898  pconnconn  35215  iccllysconn  35234  satffunlem2lem1  35388  cgrextend  35989  btwnexch2  36004  colineardim1  36042  lineext  36057  btwnconn1lem13  36080  btwnconn1lem14  36081  seglecgr12im  36091  outsideofeq  36111  outsideofeu  36112  nn0prpwlem  36304  neibastop2lem  36342  tailfb  36359  nndivsub  36439  ee7.2aOLD  36443  fvineqsneu  37393  poimirlem31  37637  heicant  37641  filbcmb  37726  prdsbnd2  37781  heibor  37807  rngoisocnv  37967  ax12eq  38922  ax12el  38923  pmodlem2  39829  cdleme22b  40323  cdleme32d  40426  cdleme32f  40428  trlord  40551  cdlemj2  40804  cdlemk38  40897  cdlemk19x  40925  dihord2pre  41207  fsuppind  42576  mzpcompact2lem  42738  pellfundex  42873  acongsym  42964  pwssplit4  43077  pwslnm  43082  cantnfresb  43313  relexpmulg  43699  stoweidlem17  45972  2reu8i  47062  imasetpreimafvbijlemf1  47328  iccpartigtl  47347  paireqne  47435  fmtnofac2lem  47492  2pwp1prmfmtno  47514  lighneallem4  47534  bgoldbtbndlem2  47730  bgoldbtbndlem3  47731  bgoldbtbnd  47733  isuspgrimlem  47811  grimco  47817  isubgr3stgrlem6  47873  lmod0rng  48072  2zrngamgm  48088