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  5650  f0rn0  6762  funfvima3  7227  dff14i  7251  isomin  7329  isoini  7330  ovg  7570  elovmpt3rab1  7665  onint  7782  peano5  7887  poseq  8155  tfrlem11  8400  tz7.48lem  8453  oalimcl  8570  oaass  8571  resixpfo  8948  fundmen  9043  ssfiALT  9186  php3  9221  php3OLD  9231  fodomfi  9320  fodomfiOLD  9340  marypha1lem  9443  card2inf  9567  ixpiunwdom  9602  cantnflt  9684  cnfcom  9712  dfac3  10133  dfac5lem5  10139  dfac5  10141  cfcoflem  10284  fin1a2s  10426  zorn2lem4  10511  zorn2lem7  10514  fpwwe2lem11  10653  wunfi  10733  grur1a  10831  addcanpi  10911  mulcanpi  10912  distrlem1pr  11037  ltaddpr  11046  ltexprlem1  11048  ltexprlem6  11053  ltexprlem7  11054  prodgt0  12086  mulgt1OLD  12098  uzwo  12925  xmulasslem  13299  xlemul1a  13302  faclbnd  14306  swrdwrdsymb  14678  pfxccatin12lem2a  14743  pfxccat3  14750  swrdccat  14751  cshwidxmod  14819  s3iunsndisj  14985  dvdsaddre2b  16324  divgcdcoprm0  16682  cncongr2  16685  infpnlem1  16928  isacs4lem  18552  cycsubm  19183  gsmsymgrfixlem1  19406  gsmsymgrfix  19407  imasabl  19855  dmdprdsplit2lem  20026  pgpfac1  20061  pgpfac  20065  lssssr  20909  islmhm2  20994  lspdisj  21084  pzriprnglem5  21444  pzriprnglem8  21447  cygznlem2a  21526  lindfmm  21785  scmataddcl  22452  scmatsubcl  22453  scmatmulcl  22454  cpmatacl  22652  cayhamlem3  22823  cayleyhamilton1  22828  neindisj  23053  cnpnei  23200  t0dist  23261  ordthauslem  23319  uncmp  23339  fiuncmp  23340  iunconnlem  23363  fbasrn  23820  rnelfmlem  23888  rnelfm  23889  fmfnfmlem2  23891  fmfnfmlem4  23893  fclscf  23961  alexsubALTlem3  23985  alexsubALTlem4  23986  alexsubALT  23987  reconn  24766  fsumcn  24810  ovolfiniun  25452  dyadmax  25549  dyadmbllem  25550  dvmptfsum  25929  dvlip2  25950  dvivthlem1  25963  dvcnvrelem1  25972  ply1divex  26092  fta1g  26125  plydivex  26255  fta1  26266  mulcxp  26644  zabsle1  27257  lgsquad2lem2  27346  2lgsoddprm  27377  pntlem3  27570  nodenselem8  27653  nocvxmin  27740  precsexlem11  28158  om2noseqrdg  28227  brbtwn  28824  brcgr  28825  brbtwn2  28830  axeuclid  28888  finsumvtxdg2size  29476  uhgrwkspthlem2  29682  crctcshwlkn0  29749  wwlksnred  29820  wwlksnextinj  29827  umgr2wlk  29877  elwwlks2  29894  clwlkclwwlklem2a  29925  clwlkclwwlkf1lem3  29933  eupth2lems  30165  numclwwlk2lem1lem  30269  frgrregord013  30322  grpoidinvlem3  30433  shorth  31222  pjhthmo  31229  pjpjpre  31346  elspansn5  31501  lnopmi  31927  adjlnop  32013  leopmul2i  32062  stlesi  32168  ssmd2  32239  dmdsl3  32242  mdexchi  32262  cvexchlem  32295  atcv1  32307  atcvatlem  32312  atabsi  32328  mdsymlem2  32331  mdsymlem5  32334  sumdmdii  32342  sumdmdlem  32345  sumdmdlem2  32346  dya2iocnrect  34259  bnj571  34883  pconnconn  35199  iccllysconn  35218  satffunlem2lem1  35372  cgrextend  35972  btwnexch2  35987  colineardim1  36025  lineext  36040  btwnconn1lem13  36063  btwnconn1lem14  36064  seglecgr12im  36074  outsideofeq  36094  outsideofeu  36095  nn0prpwlem  36286  neibastop2lem  36324  tailfb  36341  nndivsub  36421  ee7.2aOLD  36425  fvineqsneu  37375  poimirlem31  37621  heicant  37625  filbcmb  37710  prdsbnd2  37765  heibor  37791  rngoisocnv  37951  ax12eq  38905  ax12el  38906  pmodlem2  39812  cdleme22b  40306  cdleme32d  40409  cdleme32f  40411  trlord  40534  cdlemj2  40787  cdlemk38  40880  cdlemk19x  40908  dihord2pre  41190  fsuppind  42560  mzpcompact2lem  42721  pellfundex  42856  acongsym  42947  pwssplit4  43060  pwslnm  43065  cantnfresb  43295  relexpmulg  43681  relpmin  44925  stoweidlem17  45994  2reu8i  47090  imasetpreimafvbijlemf1  47366  iccpartigtl  47385  paireqne  47473  fmtnofac2lem  47530  2pwp1prmfmtno  47552  lighneallem4  47572  bgoldbtbndlem2  47768  bgoldbtbndlem3  47769  bgoldbtbnd  47771  grimco  47850  isuspgrimlem  47856  cycl3grtri  47907  isubgr3stgrlem6  47931  lmod0rng  48152  2zrngamgm  48168