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  5612  f0rn0  6708  funfvima3  7170  dff14i  7193  isomin  7271  isoini  7272  ovg  7511  elovmpt3rab1  7606  onint  7723  peano5  7823  poseq  8088  tfrlem11  8307  tz7.48lem  8360  oalimcl  8475  oaass  8476  resixpfo  8860  fundmen  8953  ssfiALT  9083  php3  9118  fodomfi  9196  fodomfiOLD  9214  marypha1lem  9317  card2inf  9441  ixpiunwdom  9476  cantnflt  9562  cnfcom  9590  dfac3  10009  dfac5lem5  10015  dfac5  10017  cfcoflem  10160  fin1a2s  10302  zorn2lem4  10387  zorn2lem7  10390  fpwwe2lem11  10529  wunfi  10609  grur1a  10707  addcanpi  10787  mulcanpi  10788  distrlem1pr  10913  ltaddpr  10922  ltexprlem1  10924  ltexprlem6  10929  ltexprlem7  10930  prodgt0  11965  mulgt1OLD  11977  uzwo  12806  xmulasslem  13181  xlemul1a  13184  faclbnd  14194  swrdwrdsymb  14567  pfxccatin12lem2a  14631  pfxccat3  14638  swrdccat  14639  cshwidxmod  14707  s3iunsndisj  14872  dvdsaddre2b  16215  divgcdcoprm0  16573  cncongr2  16576  infpnlem1  16819  isacs4lem  18447  cycsubm  19112  gsmsymgrfixlem1  19337  gsmsymgrfix  19338  imasabl  19786  dmdprdsplit2lem  19957  pgpfac1  19992  pgpfac  19996  lssssr  20885  islmhm2  20970  lspdisj  21060  pzriprnglem5  21420  pzriprnglem8  21423  cygznlem2a  21502  lindfmm  21762  scmataddcl  22429  scmatsubcl  22430  scmatmulcl  22431  cpmatacl  22629  cayhamlem3  22800  cayleyhamilton1  22805  neindisj  23030  cnpnei  23177  t0dist  23238  ordthauslem  23296  uncmp  23316  fiuncmp  23317  iunconnlem  23340  fbasrn  23797  rnelfmlem  23865  rnelfm  23866  fmfnfmlem2  23868  fmfnfmlem4  23870  fclscf  23938  alexsubALTlem3  23962  alexsubALTlem4  23963  alexsubALT  23964  reconn  24742  fsumcn  24786  ovolfiniun  25427  dyadmax  25524  dyadmbllem  25525  dvmptfsum  25904  dvlip2  25925  dvivthlem1  25938  dvcnvrelem1  25947  ply1divex  26067  fta1g  26100  plydivex  26230  fta1  26241  mulcxp  26619  zabsle1  27232  lgsquad2lem2  27321  2lgsoddprm  27352  pntlem3  27545  nodenselem8  27628  nocvxmin  27716  precsexlem11  28153  om2noseqrdg  28232  expadds  28356  brbtwn  28875  brcgr  28876  brbtwn2  28881  axeuclid  28939  finsumvtxdg2size  29527  uhgrwkspthlem2  29730  crctcshwlkn0  29797  wwlksnred  29868  wwlksnextinj  29875  umgr2wlk  29925  elwwlks2  29942  clwlkclwwlklem2a  29973  clwlkclwwlkf1lem3  29981  eupth2lems  30213  numclwwlk2lem1lem  30317  frgrregord013  30370  grpoidinvlem3  30481  shorth  31270  pjhthmo  31277  pjpjpre  31394  elspansn5  31549  lnopmi  31975  adjlnop  32061  leopmul2i  32110  stlesi  32216  ssmd2  32287  dmdsl3  32290  mdexchi  32310  cvexchlem  32343  atcv1  32355  atcvatlem  32360  atabsi  32376  mdsymlem2  32379  mdsymlem5  32382  sumdmdii  32390  sumdmdlem  32393  sumdmdlem2  32394  dya2iocnrect  34289  bnj571  34913  pconnconn  35263  iccllysconn  35282  satffunlem2lem1  35436  cgrextend  36041  btwnexch2  36056  colineardim1  36094  lineext  36109  btwnconn1lem13  36132  btwnconn1lem14  36133  seglecgr12im  36143  outsideofeq  36163  outsideofeu  36164  nn0prpwlem  36355  neibastop2lem  36393  tailfb  36410  nndivsub  36490  ee7.2aOLD  36494  fvineqsneu  37444  poimirlem31  37690  heicant  37694  filbcmb  37779  prdsbnd2  37834  heibor  37860  rngoisocnv  38020  ax12eq  38979  ax12el  38980  pmodlem2  39885  cdleme22b  40379  cdleme32d  40482  cdleme32f  40484  trlord  40607  cdlemj2  40860  cdlemk38  40953  cdlemk19x  40981  dihord2pre  41263  fsuppind  42622  mzpcompact2lem  42783  pellfundex  42918  acongsym  43008  pwssplit4  43121  pwslnm  43126  cantnfresb  43356  relexpmulg  43742  relpmin  44984  stoweidlem17  46054  2reu8i  47143  imasetpreimafvbijlemf1  47434  iccpartigtl  47453  paireqne  47541  fmtnofac2lem  47598  2pwp1prmfmtno  47620  lighneallem4  47640  bgoldbtbndlem2  47836  bgoldbtbndlem3  47837  bgoldbtbnd  47839  grimco  47919  isuspgrimlem  47925  cycl3grtri  47977  isubgr3stgrlem6  48001  lmod0rng  48259  2zrngamgm  48275