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  5655  f0rn0  6764  funfvima3  7239  dff14i  7260  isomin  7342  isoini  7343  ovg  7582  elovmpt3rab1  7678  onint  7793  peano5  7894  poseq  8160  tfrlem11  8381  tz7.48lem  8434  oalimcl  8551  oaass  8552  resixpfo  8947  fundmen  9042  ssfiALT  9172  php3  9207  fodomfi  9286  marypha1lem  9407  card2inf  9531  ixpiunwdom  9566  cantnflt  9655  cnfcom  9683  dfac3  10128  dfac5lem5  10134  dfac5  10135  cfcoflem  10278  fin1a2s  10420  zorn2lem4  10505  zorn2lem7  10508  fpwwe2lem11  10654  wunfi  10734  grur1a  10832  addcanpi  10912  mulcanpi  10913  distrlem1pr  11038  ltaddpr  11047  ltexprlem1  11049  ltexprlem6  11054  ltexprlem7  11055  prodgt0  12090  uzwo  12964  xmulasslem  13341  xlemul1a  13344  faclbnd  14358  swrdwrdsymb  14736  pfxccatin12lem2a  14800  pfxccat3  14807  swrdccat  14808  cshwidxmod  14878  s3iunsndisj  15045  dvdsaddre2b  16403  divgcdcoprm0  16761  cncongr2  16764  infpnlem1  17008  isacs4lem  18638  cycsubm  19336  gsmsymgrfixlem1  19560  gsmsymgrfix  19561  imasabl  20009  dmdprdsplit2lem  20180  pgpfac1  20215  pgpfac  20219  isdrng3lem2  20921  lssssr  21144  islmhm2  21228  lspdisj  21318  pzriprnglem5  21704  pzriprnglem8  21707  cygznlem2a  21786  lindfmm  22046  scmataddcl  22744  scmatsubcl  22745  scmatmulcl  22746  cpmatacl  22947  cayhamlem3  23118  cayleyhamilton1  23123  neindisj  23348  cnpnei  23495  t0dist  23556  ordthauslem  23614  uncmp  23634  fiuncmp  23635  iunconnlem  23658  fbasrn  24116  rnelfmlem  24184  rnelfm  24185  fmfnfmlem2  24187  fmfnfmlem4  24189  fclscf  24257  alexsubALTlem3  24281  alexsubALTlem4  24282  alexsubALT  24283  reconn  25061  fsumcn  25104  ovolfiniun  25735  dyadmax  25832  dyadmbllem  25833  dvmptfsum  26209  dvlip2  26229  dvivthlem1  26242  dvcnvrelem1  26251  ply1divex  26369  fta1g  26402  plydivex  26534  fta1  26545  mulcxp  26930  zabsle1  27540  lgsquad2lem2  27629  2lgsoddprm  27660  pntlem3  27853  nodenselem8  27935  nocvxmin  28028  precsexlem11  28490  om2noseqrdg  28577  expadds  28708  brbtwn  29364  brcgr  29365  brbtwn2  29370  axeuclid  29428  finsumvtxdg2size  30018  uhgrwkspthlem2  30227  crctcshwlkn0  30297  wwlksnred  30368  wwlksnextinj  30375  umgr2wlk  30425  elwwlks2  30445  clwlkclwwlklem2a  30476  clwlkclwwlkf1lem3  30484  eupth2lems  30726  numclwwlk2lem1lem  30830  frgrregord013  30883  grpoidinvlem3  30995  shorth  31784  pjhthmo  31791  pjpjpre  31908  elspansn5  32063  lnopmi  32489  adjlnop  32575  leopmul2i  32624  stlesi  32730  ssmd2  32801  dmdsl3  32804  mdexchi  32824  cvexchlem  32857  atcv1  32869  atcvatlem  32874  atabsi  32890  mdsymlem2  32893  mdsymlem5  32896  sumdmdii  32904  sumdmdlem  32907  sumdmdlem2  32908  dya2iocnrect  34800  bnj571  35423  pconnconn  35818  iccllysconn  35837  satffunlem2lem1  35991  cgrextend  36596  btwnexch2  36611  colineardim1  36649  lineext  36664  btwnconn1lem13  36687  btwnconn1lem14  36688  seglecgr12im  36698  outsideofeq  36718  outsideofeu  36719  nn0prpwlem  36949  neibastop2lem  36987  tailfb  37004  nndivsub  37084  ee7.2aOLD  37088  fvineqsneu  38173  poimirlem31  38408  heicant  38412  filbcmb  38498  prdsbnd2  38553  heibor  38579  rngoisocnv  38739  ax12eq  39822  ax12el  39823  pmodlem2  40728  cdleme22b  41222  cdleme32d  41325  cdleme32f  41327  trlord  41450  cdlemj2  41703  cdlemk38  41796  cdlemk19x  41824  dihord2pre  42106  fsuppind  43444  mzpcompact2lem  43604  pellfundex  43735  acongsym  43825  pwssplit4  43938  pwslnm  43943  cantnfresb  44173  relexpmulg  44558  relpmin  45783  stoweidlem17  46853  2reu8i  48009  imasetpreimafvbijlemf1  48312  iccpartigtl  48331  paireqne  48419  fmtnofac2lem  48479  2pwp1prmfmtno  48501  lighneallem4  48521  bgoldbtbndlem2  48730  bgoldbtbndlem3  48731  bgoldbtbnd  48733  grimco  48813  isuspgrimlem  48819  cycl3grtri  48871  isubgr3stgrlem6  48895  lmod0rng  49152  2zrngamgm  49168