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  5646  f0rn0  6768  funfvima3  7243  dff14i  7264  isomin  7346  isoini  7347  ovg  7586  elovmpt3rab1  7682  onint  7805  peano5  7906  poseq  8178  tfrlem11  8400  tz7.48lemOLD  8455  oalimcl  8572  oaass  8573  resixpfo  8968  fundmen  9063  ssfiALT  9193  php3  9228  fodomfi  9308  marypha1lem  9429  card2inf  9553  ixpiunwdom  9588  cantnflt  9677  cnfcom  9705  dfac3  10204  dfac5lem5  10210  dfac5  10211  cfcoflem  10354  fin1a2s  10496  zorn2lem4  10581  zorn2lem7  10584  fpwwe2lem11  10730  wunfi  10810  grur1a  10908  addcanpi  10988  mulcanpi  10989  distrlem1pr  11114  ltaddpr  11123  ltexprlem1  11125  ltexprlem6  11130  ltexprlem7  11131  prodgt0  12168  uzwo  13042  xmulasslem  13419  xlemul1a  13422  faclbnd  14438  swrdwrdsymb  14817  pfxccatin12lem2a  14881  pfxccat3  14888  swrdccat  14889  cshwidxmod  14959  s3iunsndisj  15127  dvdsaddre2b  16483  divgcdcoprm0  16846  cncongr2  16849  infpnlem1  17094  isacs4lem  18724  cycsubm  19423  gsmsymgrfixlem1  19647  gsmsymgrfix  19648  imasabl  20096  dmdprdsplit2lem  20267  pgpfac1  20302  pgpfac  20306  isdrng3lem2  21012  lssssr  21235  islmhm2  21319  lspdisj  21409  pzriprnglem5  21797  pzriprnglem8  21800  cygznlem2a  21879  lindfmm  22139  scmataddcl  22837  scmatsubcl  22838  scmatmulcl  22839  cpmatacl  23040  cayhamlem3  23211  cayleyhamilton1  23216  neindisj  23441  cnpnei  23588  t0dist  23649  ordthauslem  23707  uncmp  23727  fiuncmp  23728  iunconnlem  23751  fbasrn  24209  rnelfmlem  24277  rnelfm  24278  fmfnfmlem2  24280  fmfnfmlem4  24282  fclscf  24350  alexsubALTlem3  24374  alexsubALTlem4  24375  alexsubALT  24376  reconn  25154  fsumcn  25197  ovolfiniun  25828  dyadmax  25925  dyadmbllem  25926  dvmptfsum  26301  dvlip2  26321  dvivthlem1  26334  dvcnvrelem1  26343  ply1divex  26461  fta1g  26494  plydivex  26624  fta1  26635  mulcxp  27019  zabsle1  27629  lgsquad2lem2  27718  2lgsoddprm  27749  pntlem3  27942  nodenselem8  28054  nocvxmin  28147  precsexlem11  28609  om2noseqrdg  28696  expadds  28827  brbtwn  29483  brcgr  29484  brbtwn2  29489  axeuclid  29547  finsumvtxdg2size  30137  uhgrwkspthlem2  30346  crctcshwlkn0  30416  wwlksnred  30487  wwlksnextinj  30494  umgr2wlk  30544  elwwlks2  30564  clwlkclwwlklem2a  30595  clwlkclwwlkf1lem3  30603  eupth2lems  30845  numclwwlk2lem1lem  30949  frgrregord013  31002  grpoidinvlem3  31114  shorth  31903  pjhthmo  31910  pjpjpre  32027  elspansn5  32182  lnopmi  32608  adjlnop  32694  leopmul2i  32743  stlesi  32849  ssmd2  32920  dmdsl3  32923  mdexchi  32943  cvexchlem  32976  atcv1  32988  atcvatlem  32993  atabsi  33009  mdsymlem2  33012  mdsymlem5  33015  sumdmdii  33023  sumdmdlem  33026  sumdmdlem2  33027  dya2iocnrect  34960  bnj571  35583  pconnconn  36083  iccllysconn  36102  satffunlem2lem1  36256  cgrextend  36866  btwnexch2  36881  colineardim1  36919  lineext  36934  btwnconn1lem13  36957  btwnconn1lem14  36958  seglecgr12im  36968  outsideofeq  36988  outsideofeu  36989  nn0prpwlem  37203  neibastop2lem  37241  tailfb  37258  nndivsub  37338  ee7.2aOLD  37342  fvineqsneu  38428  poimirlem31  38663  heicant  38667  filbcmb  38768  prdsbnd2  38823  heibor  38849  rngoisocnv  39009  ax12eq  40092  ax12el  40093  pmodlem2  40998  cdleme22b  41492  cdleme32d  41595  cdleme32f  41597  trlord  41720  cdlemj2  41973  cdlemk38  42066  cdlemk19x  42094  dihord2pre  42376  fsuppind  43712  mzpcompact2lem  43856  pellfundex  43987  acongsym  44077  pwssplit4  44185  pwslnm  44190  cantnfresb  44420  relexpmulg  44804  relpmin  46036  stoweidlem17  47121  2reu8i  48277  imasetpreimafvbijlemf1  48580  iccpartigtl  48599  paireqne  48687  fmtnofac2lem  48747  2pwp1prmfmtno  48769  lighneallem4  48789  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  bgoldbtbnd  49001  grimco  49081  isuspgrimlem  49087  cycl3grtri  49139  isubgr3stgrlem6  49163  lmod0rng  49420  2zrngamgm  49436