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  5661  f0rn0  6773  funfvima3  7238  isomin  7339  isoini  7340  ovg  7580  elovmpt3rab1  7675  onint  7792  peano5  7897  poseq  8165  tfrlem11  8410  tz7.48lem  8463  oalimcl  8580  oaass  8581  resixpfo  8958  fundmen  9053  ssfiALT  9196  php3  9231  php3OLD  9243  fodomfi  9332  fodomfiOLD  9352  marypha1lem  9455  card2inf  9577  ixpiunwdom  9612  cantnflt  9694  cnfcom  9722  dfac3  10143  dfac5lem5  10149  dfac5  10151  cfcoflem  10294  fin1a2s  10436  zorn2lem4  10521  zorn2lem7  10524  fpwwe2lem11  10663  wunfi  10743  grur1a  10841  addcanpi  10921  mulcanpi  10922  distrlem1pr  11047  ltaddpr  11056  ltexprlem1  11058  ltexprlem6  11063  ltexprlem7  11064  prodgt0  12096  mulgt1OLD  12108  uzwo  12935  xmulasslem  13309  xlemul1a  13312  faclbnd  14312  swrdwrdsymb  14683  pfxccatin12lem2a  14748  pfxccat3  14755  swrdccat  14756  cshwidxmod  14824  s3iunsndisj  14990  dvdsaddre2b  16327  divgcdcoprm0  16685  cncongr2  16688  infpnlem1  16931  isacs4lem  18559  cycsubm  19190  gsmsymgrfixlem1  19414  gsmsymgrfix  19415  imasabl  19863  dmdprdsplit2lem  20034  pgpfac1  20069  pgpfac  20073  lssssr  20921  islmhm2  21006  lspdisj  21096  pzriprnglem5  21459  pzriprnglem8  21462  cygznlem2a  21541  lindfmm  21802  scmataddcl  22471  scmatsubcl  22472  scmatmulcl  22473  cpmatacl  22671  cayhamlem3  22842  cayleyhamilton1  22847  neindisj  23072  cnpnei  23219  t0dist  23280  ordthauslem  23338  uncmp  23358  fiuncmp  23359  iunconnlem  23382  fbasrn  23839  rnelfmlem  23907  rnelfm  23908  fmfnfmlem2  23910  fmfnfmlem4  23912  fclscf  23980  alexsubALTlem3  24004  alexsubALTlem4  24005  alexsubALT  24006  reconn  24787  fsumcn  24831  ovolfiniun  25473  dyadmax  25570  dyadmbllem  25571  dvmptfsum  25950  dvlip2  25971  dvivthlem1  25984  dvcnvrelem1  25993  ply1divex  26113  fta1g  26146  plydivex  26276  fta1  26287  mulcxp  26664  zabsle1  27277  lgsquad2lem2  27366  2lgsoddprm  27397  pntlem3  27590  nodenselem8  27673  nocvxmin  27760  precsexlem11  28178  om2noseqrdg  28247  brbtwn  28845  brcgr  28846  brbtwn2  28851  axeuclid  28909  finsumvtxdg2size  29497  uhgrwkspthlem2  29703  crctcshwlkn0  29770  wwlksnred  29841  wwlksnextinj  29848  umgr2wlk  29898  elwwlks2  29915  clwlkclwwlklem2a  29946  clwlkclwwlkf1lem3  29954  eupth2lems  30186  numclwwlk2lem1lem  30290  frgrregord013  30343  grpoidinvlem3  30454  shorth  31243  pjhthmo  31250  pjpjpre  31367  elspansn5  31522  lnopmi  31948  adjlnop  32034  leopmul2i  32083  stlesi  32189  ssmd2  32260  dmdsl3  32263  mdexchi  32283  cvexchlem  32316  atcv1  32328  atcvatlem  32333  atabsi  32349  mdsymlem2  32352  mdsymlem5  32355  sumdmdii  32363  sumdmdlem  32366  sumdmdlem2  32367  dya2iocnrect  34258  bnj571  34895  pconnconn  35211  iccllysconn  35230  satffunlem2lem1  35384  cgrextend  35984  btwnexch2  35999  colineardim1  36037  lineext  36052  btwnconn1lem13  36075  btwnconn1lem14  36076  seglecgr12im  36086  outsideofeq  36106  outsideofeu  36107  nn0prpwlem  36298  neibastop2lem  36336  tailfb  36353  nndivsub  36433  ee7.2aOLD  36437  fvineqsneu  37387  poimirlem31  37633  heicant  37637  filbcmb  37722  prdsbnd2  37777  heibor  37803  rngoisocnv  37963  ax12eq  38917  ax12el  38918  pmodlem2  39824  cdleme22b  40318  cdleme32d  40421  cdleme32f  40423  trlord  40546  cdlemj2  40799  cdlemk38  40892  cdlemk19x  40920  dihord2pre  41202  fsuppind  42579  mzpcompact2lem  42740  pellfundex  42875  acongsym  42966  pwssplit4  43079  pwslnm  43084  cantnfresb  43314  relexpmulg  43700  relpmin  44945  stoweidlem17  46004  2reu8i  47098  imasetpreimafvbijlemf1  47364  iccpartigtl  47383  paireqne  47471  fmtnofac2lem  47528  2pwp1prmfmtno  47550  lighneallem4  47570  bgoldbtbndlem2  47766  bgoldbtbndlem3  47767  bgoldbtbnd  47769  isuspgrimlem  47847  grimco  47853  cycl3grtri  47887  isubgr3stgrlem6  47911  lmod0rng  48118  2zrngamgm  48134