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  5647  f0rn0  6759  funfvima3  7234  dff14i  7255  isomin  7337  isoini  7338  ovg  7577  elovmpt3rab1  7673  onint  7793  peano5  7894  poseq  8159  tfrlem11  8380  tz7.48lemOLD  8435  oalimcl  8552  oaass  8553  resixpfo  8948  fundmen  9043  ssfiALT  9173  php3  9208  fodomfi  9288  marypha1lem  9409  card2inf  9533  ixpiunwdom  9568  cantnflt  9657  cnfcom  9685  dfac3  10181  dfac5lem5  10187  dfac5  10188  cfcoflem  10331  fin1a2s  10473  zorn2lem4  10558  zorn2lem7  10561  fpwwe2lem11  10707  wunfi  10787  grur1a  10885  addcanpi  10965  mulcanpi  10966  distrlem1pr  11091  ltaddpr  11100  ltexprlem1  11102  ltexprlem6  11107  ltexprlem7  11108  prodgt0  12145  uzwo  13019  xmulasslem  13396  xlemul1a  13399  faclbnd  14414  swrdwrdsymb  14792  pfxccatin12lem2a  14856  pfxccat3  14863  swrdccat  14864  cshwidxmod  14934  s3iunsndisj  15101  dvdsaddre2b  16457  divgcdcoprm0  16820  cncongr2  16823  infpnlem1  17068  isacs4lem  18698  cycsubm  19397  gsmsymgrfixlem1  19621  gsmsymgrfix  19622  imasabl  20070  dmdprdsplit2lem  20241  pgpfac1  20276  pgpfac  20280  isdrng3lem2  20986  lssssr  21209  islmhm2  21293  lspdisj  21383  pzriprnglem5  21771  pzriprnglem8  21774  cygznlem2a  21853  lindfmm  22113  scmataddcl  22811  scmatsubcl  22812  scmatmulcl  22813  cpmatacl  23014  cayhamlem3  23185  cayleyhamilton1  23190  neindisj  23415  cnpnei  23562  t0dist  23623  ordthauslem  23681  uncmp  23701  fiuncmp  23702  iunconnlem  23725  fbasrn  24183  rnelfmlem  24251  rnelfm  24252  fmfnfmlem2  24254  fmfnfmlem4  24256  fclscf  24324  alexsubALTlem3  24348  alexsubALTlem4  24349  alexsubALT  24350  reconn  25128  fsumcn  25171  ovolfiniun  25802  dyadmax  25899  dyadmbllem  25900  dvmptfsum  26275  dvlip2  26295  dvivthlem1  26308  dvcnvrelem1  26317  ply1divex  26435  fta1g  26468  plydivex  26600  fta1  26611  mulcxp  26995  zabsle1  27605  lgsquad2lem2  27694  2lgsoddprm  27725  pntlem3  27918  nodenselem8  28030  nocvxmin  28123  precsexlem11  28585  om2noseqrdg  28672  expadds  28803  brbtwn  29459  brcgr  29460  brbtwn2  29465  axeuclid  29523  finsumvtxdg2size  30113  uhgrwkspthlem2  30322  crctcshwlkn0  30392  wwlksnred  30463  wwlksnextinj  30470  umgr2wlk  30520  elwwlks2  30540  clwlkclwwlklem2a  30571  clwlkclwwlkf1lem3  30579  eupth2lems  30821  numclwwlk2lem1lem  30925  frgrregord013  30978  grpoidinvlem3  31090  shorth  31879  pjhthmo  31886  pjpjpre  32003  elspansn5  32158  lnopmi  32584  adjlnop  32670  leopmul2i  32719  stlesi  32825  ssmd2  32896  dmdsl3  32899  mdexchi  32919  cvexchlem  32952  atcv1  32964  atcvatlem  32969  atabsi  32985  mdsymlem2  32988  mdsymlem5  32991  sumdmdii  32999  sumdmdlem  33002  sumdmdlem2  33003  dya2iocnrect  34896  bnj571  35519  pconnconn  35965  iccllysconn  35984  satffunlem2lem1  36138  cgrextend  36743  btwnexch2  36758  colineardim1  36796  lineext  36811  btwnconn1lem13  36834  btwnconn1lem14  36835  seglecgr12im  36845  outsideofeq  36865  outsideofeu  36866  nn0prpwlem  37080  neibastop2lem  37118  tailfb  37135  nndivsub  37215  ee7.2aOLD  37219  fvineqsneu  38302  poimirlem31  38537  heicant  38541  filbcmb  38642  prdsbnd2  38697  heibor  38723  rngoisocnv  38883  ax12eq  39966  ax12el  39967  pmodlem2  40872  cdleme22b  41366  cdleme32d  41469  cdleme32f  41471  trlord  41594  cdlemj2  41847  cdlemk38  41940  cdlemk19x  41968  dihord2pre  42250  fsuppind  43580  mzpcompact2lem  43715  pellfundex  43846  acongsym  43936  pwssplit4  44049  pwslnm  44054  cantnfresb  44284  relexpmulg  44669  relpmin  45894  stoweidlem17  46971  2reu8i  48127  imasetpreimafvbijlemf1  48430  iccpartigtl  48449  paireqne  48537  fmtnofac2lem  48597  2pwp1prmfmtno  48619  lighneallem4  48639  bgoldbtbndlem2  48848  bgoldbtbndlem3  48849  bgoldbtbnd  48851  grimco  48931  isuspgrimlem  48937  cycl3grtri  48989  isubgr3stgrlem6  49013  lmod0rng  49270  2zrngamgm  49286