Theorem exp32 426

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 418	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 421	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  exp44  443  exp45  444  expr  462  anassrs  473  an13s  664  3impb  1132  wereu  5652  f0rn0  6792  funfvima3  7268  dff14i  7289  isomin  7371  isoini  7372  ovg  7612  elovmpt3rab1  7708  onint  7831  peano5  7932  poseq  8205  tfrlem11  8427  tz7.48lemOLD  8482  oalimcl  8599  oaass  8600  resixpfo  8995  fundmen  9090  ssfiALT  9220  php3  9255  fodomfi  9335  marypha1lem  9455  card2inf  9579  ixpiunwdom  9614  cantnflt  9703  cnfcom  9731  dfac3  10230  dfac5lem5  10236  dfac5  10237  cfcoflem  10380  fin1a2s  10522  zorn2lem4  10607  zorn2lem7  10610  fpwwe2lem11  10756  wunfi  10836  grur1a  10934  addcanpi  11014  mulcanpi  11015  distrlem1pr  11140  ltaddpr  11149  ltexprlem1  11151  ltexprlem6  11156  ltexprlem7  11157  prodgt0  12194  uzwo  13068  xmulasslem  13445  xlemul1a  13448  faclbnd  14464  swrdwrdsymb  14843  pfxccatin12lem2a  14907  pfxccat3  14914  swrdccat  14915  cshwidxmod  14985  s3iunsndisj  15153  dvdsaddre2b  16509  divgcdcoprm0  16872  cncongr2  16875  infpnlem1  17120  isacs4lem  18750  cycsubm  19449  gsmsymgrfixlem1  19674  gsmsymgrfix  19675  imasabl  20123  dmdprdsplit2lem  20294  pgpfac1  20329  pgpfac  20333  isdrng3lem2  21039  lssssr  21262  islmhm2  21346  lspdisj  21436  pzriprnglem5  21824  pzriprnglem8  21827  cygznlem2a  21906  lindfmm  22166  scmataddcl  22864  scmatsubcl  22865  scmatmulcl  22866  cpmatacl  23067  cayhamlem3  23238  cayleyhamilton1  23243  neindisj  23468  cnpnei  23615  t0dist  23676  ordthauslem  23734  uncmp  23754  fiuncmp  23755  iunconnlem  23778  fbasrn  24236  rnelfmlem  24304  rnelfm  24305  fmfnfmlem2  24307  fmfnfmlem4  24309  fclscf  24377  alexsubALTlem3  24401  alexsubALTlem4  24402  alexsubALT  24403  reconn  25181  fsumcn  25224  ovolfiniun  25855  dyadmax  25952  dyadmbllem  25953  dvmptfsum  26328  dvlip2  26348  dvivthlem1  26361  dvcnvrelem1  26370  ply1divex  26488  fta1g  26521  plydivex  26651  fta1  26662  mulcxp  27046  zabsle1  27656  lgsquad2lem2  27745  2lgsoddprm  27776  pntlem3  27969  nodenselem8  28081  nocvxmin  28174  precsexlem11  28636  om2noseqrdg  28723  expadds  28854  brbtwn  29510  brcgr  29511  brbtwn2  29516  axeuclid  29574  finsumvtxdg2size  30164  uhgrwkspthlem2  30373  crctcshwlkn0  30443  wwlksnred  30514  wwlksnextinj  30521  umgr2wlk  30571  elwwlks2  30591  clwlkclwwlklem2a  30622  clwlkclwwlkf1lem3  30630  eupth2lems  30872  numclwwlk2lem1lem  30976  frgrregord013  31029  grpoidinvlem3  31141  shorth  31930  pjhthmo  31937  pjpjpre  32054  elspansn5  32209  lnopmi  32635  adjlnop  32721  leopmul2i  32770  stlesi  32876  ssmd2  32947  dmdsl3  32950  mdexchi  32970  cvexchlem  33003  atcv1  33015  atcvatlem  33020  atabsi  33036  mdsymlem2  33039  mdsymlem5  33042  sumdmdii  33050  sumdmdlem  33053  sumdmdlem2  33054  dya2iocnrect  34996  bnj571  35619  pconnconn  36176  iccllysconn  36195  satffunlem2lem1  36349  cgrextend  36964  btwnexch2  36979  colineardim1  37017  lineext  37032  btwnconn1lem13  37055  btwnconn1lem14  37056  seglecgr12im  37066  outsideofeq  37086  outsideofeu  37087  nn0prpwlem  37301  neibastop2lem  37339  tailfb  37356  nndivsub  37436  ee7.2aOLD  37440  fvineqsneu  38539  poimirlem31  38774  heicant  38778  filbcmb  38877  prdsbnd2  38932  heibor  38958  rngoisocnv  39118  ax12eq  40201  ax12el  40202  pmodlem2  41107  cdleme22b  41601  cdleme32d  41704  cdleme32f  41706  trlord  41829  cdlemj2  42082  cdlemk38  42175  cdlemk19x  42203  dihord2pre  42485  fsuppind  43822  mzpcompact2lem  43966  pellfundex  44097  acongsym  44187  pwssplit4  44295  pwslnm  44300  cantnfresb  44529  relexpmulg  44913  relpmin  46148  stoweidlem17  47242  2reu8i  48399  imasetpreimafvbijlemf1  48701  iccpartigtl  48720  paireqne  48808  fmtnofac2lem  48868  2pwp1prmfmtno  48890  lighneallem4  48910  bgoldbtbndlem2  49119  bgoldbtbndlem3  49120  bgoldbtbnd  49122  grimco  49202  isuspgrimlem  49208  cycl3grtri  49260  isubgr3stgrlem6  49284  lmod0rng  49541  2zrngamgm  49557