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  650  3impb  1115  wereu  5696  f0rn0  6806  funfvima3  7273  isomin  7373  isoini  7374  ovg  7615  elovmpt3rab1  7710  onint  7826  peano5  7932  peano5OLD  7933  poseq  8199  tfrlem11  8444  tz7.48lem  8497  oalimcl  8616  oaass  8617  resixpfo  8994  fundmen  9096  ssfiALT  9241  php3  9275  php3OLD  9287  fodomfi  9378  fodomfiOLD  9398  marypha1lem  9502  card2inf  9624  ixpiunwdom  9659  cantnflt  9741  cnfcom  9769  dfac3  10190  dfac5lem5  10196  dfac5  10198  cfcoflem  10341  fin1a2s  10483  zorn2lem4  10568  zorn2lem7  10571  fpwwe2lem11  10710  wunfi  10790  grur1a  10888  addcanpi  10968  mulcanpi  10969  distrlem1pr  11094  ltaddpr  11103  ltexprlem1  11105  ltexprlem6  11110  ltexprlem7  11111  prodgt0  12141  mulgt1OLD  12153  uzwo  12976  xmulasslem  13347  xlemul1a  13350  faclbnd  14339  swrdwrdsymb  14710  pfxccatin12lem2a  14775  pfxccat3  14782  swrdccat  14783  cshwidxmod  14851  s3iunsndisj  15017  dvdsaddre2b  16355  divgcdcoprm0  16712  cncongr2  16715  infpnlem1  16957  isacs4lem  18614  cycsubm  19242  gsmsymgrfixlem1  19469  gsmsymgrfix  19470  imasabl  19918  dmdprdsplit2lem  20089  pgpfac1  20124  pgpfac  20128  lssssr  20975  islmhm2  21060  lspdisj  21150  pzriprnglem5  21519  pzriprnglem8  21522  cygznlem2a  21609  lindfmm  21870  scmataddcl  22543  scmatsubcl  22544  scmatmulcl  22545  cpmatacl  22743  cayhamlem3  22914  cayleyhamilton1  22919  neindisj  23146  cnpnei  23293  t0dist  23354  ordthauslem  23412  uncmp  23432  fiuncmp  23433  iunconnlem  23456  fbasrn  23913  rnelfmlem  23981  rnelfm  23982  fmfnfmlem2  23984  fmfnfmlem4  23986  fclscf  24054  alexsubALTlem3  24078  alexsubALTlem4  24079  alexsubALT  24080  reconn  24869  fsumcn  24913  ovolfiniun  25555  dyadmax  25652  dyadmbllem  25653  dvmptfsum  26033  dvlip2  26054  dvivthlem1  26067  dvcnvrelem1  26076  ply1divex  26196  fta1g  26229  plydivex  26357  fta1  26368  mulcxp  26745  zabsle1  27358  lgsquad2lem2  27447  2lgsoddprm  27478  pntlem3  27671  nodenselem8  27754  nocvxmin  27841  precsexlem11  28259  om2noseqrdg  28328  brbtwn  28932  brcgr  28933  brbtwn2  28938  axeuclid  28996  finsumvtxdg2size  29586  uhgrwkspthlem2  29790  crctcshwlkn0  29854  wwlksnred  29925  wwlksnextinj  29932  umgr2wlk  29982  elwwlks2  29999  clwlkclwwlklem2a  30030  clwlkclwwlkf1lem3  30038  eupth2lems  30270  numclwwlk2lem1lem  30374  frgrregord013  30427  grpoidinvlem3  30538  shorth  31327  pjhthmo  31334  pjpjpre  31451  elspansn5  31606  lnopmi  32032  adjlnop  32118  leopmul2i  32167  stlesi  32273  ssmd2  32344  dmdsl3  32347  mdexchi  32367  cvexchlem  32400  atcv1  32412  atcvatlem  32417  atabsi  32433  mdsymlem2  32436  mdsymlem5  32439  sumdmdii  32447  sumdmdlem  32450  sumdmdlem2  32451  dya2iocnrect  34246  bnj571  34882  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  36288  neibastop2lem  36326  tailfb  36343  nndivsub  36423  ee7.2aOLD  36427  fvineqsneu  37377  poimirlem31  37611  heicant  37615  filbcmb  37700  prdsbnd2  37755  heibor  37781  rngoisocnv  37941  ax12eq  38897  ax12el  38898  pmodlem2  39804  cdleme22b  40298  cdleme32d  40401  cdleme32f  40403  trlord  40526  cdlemj2  40779  cdlemk38  40872  cdlemk19x  40900  dihord2pre  41182  fsuppind  42545  mzpcompact2lem  42707  pellfundex  42842  acongsym  42933  pwssplit4  43046  pwslnm  43051  cantnfresb  43286  relexpmulg  43672  stoweidlem17  45938  2reu8i  47028  imasetpreimafvbijlemf1  47278  iccpartigtl  47297  paireqne  47385  fmtnofac2lem  47442  2pwp1prmfmtno  47464  lighneallem4  47484  bgoldbtbndlem2  47680  bgoldbtbndlem3  47681  bgoldbtbnd  47683  isuspgrimlem  47758  grimco  47764  lmod0rng  47952  2zrngamgm  47968