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  5662  f0rn0  6770  funfvima3  7241  dff14i  7264  isomin  7346  isoini  7347  ovg  7588  elovmpt3rab1  7683  onint  7798  peano5  7899  poseq  8163  tfrlem11  8384  tz7.48lem  8437  oalimcl  8554  oaass  8555  resixpfo  8943  fundmen  9038  ssfiALT  9168  php3  9203  fodomfi  9282  marypha1lem  9403  card2inf  9527  ixpiunwdom  9562  cantnflt  9651  cnfcom  9679  dfac3  10124  dfac5lem5  10130  dfac5  10131  cfcoflem  10274  fin1a2s  10416  zorn2lem4  10501  zorn2lem7  10504  fpwwe2lem11  10644  wunfi  10724  grur1a  10822  addcanpi  10902  mulcanpi  10903  distrlem1pr  11028  ltaddpr  11037  ltexprlem1  11039  ltexprlem6  11044  ltexprlem7  11045  prodgt0  12080  uzwo  12953  xmulasslem  13329  xlemul1a  13332  faclbnd  14346  swrdwrdsymb  14724  pfxccatin12lem2a  14788  pfxccat3  14795  swrdccat  14796  cshwidxmod  14866  s3iunsndisj  15031  dvdsaddre2b  16390  divgcdcoprm0  16748  cncongr2  16751  infpnlem1  16995  isacs4lem  18625  cycsubm  19304  gsmsymgrfixlem1  19528  gsmsymgrfix  19529  imasabl  19977  dmdprdsplit2lem  20148  pgpfac1  20183  pgpfac  20187  isdrng3lem2  20889  lssssr  21112  islmhm2  21196  lspdisj  21286  pzriprnglem5  21672  pzriprnglem8  21675  cygznlem2a  21754  lindfmm  22014  scmataddcl  22710  scmatsubcl  22711  scmatmulcl  22712  cpmatacl  22910  cayhamlem3  23081  cayleyhamilton1  23086  neindisj  23311  cnpnei  23458  t0dist  23519  ordthauslem  23577  uncmp  23597  fiuncmp  23598  iunconnlem  23621  fbasrn  24078  rnelfmlem  24146  rnelfm  24147  fmfnfmlem2  24149  fmfnfmlem4  24151  fclscf  24219  alexsubALTlem3  24243  alexsubALTlem4  24244  alexsubALT  24245  reconn  25023  fsumcn  25066  ovolfiniun  25697  dyadmax  25794  dyadmbllem  25795  dvmptfsum  26171  dvlip2  26191  dvivthlem1  26204  dvcnvrelem1  26213  ply1divex  26331  fta1g  26364  plydivex  26495  fta1  26506  mulcxp  26887  zabsle1  27497  lgsquad2lem2  27586  2lgsoddprm  27617  pntlem3  27810  nodenselem8  27892  nocvxmin  27985  precsexlem11  28447  om2noseqrdg  28534  expadds  28665  brbtwn  29286  brcgr  29287  brbtwn2  29292  axeuclid  29350  finsumvtxdg2size  29937  uhgrwkspthlem2  30140  crctcshwlkn0  30207  wwlksnred  30278  wwlksnextinj  30285  umgr2wlk  30335  elwwlks2  30355  clwlkclwwlklem2a  30386  clwlkclwwlkf1lem3  30394  eupth2lems  30626  numclwwlk2lem1lem  30730  frgrregord013  30783  grpoidinvlem3  30895  shorth  31684  pjhthmo  31691  pjpjpre  31808  elspansn5  31963  lnopmi  32389  adjlnop  32475  leopmul2i  32524  stlesi  32630  ssmd2  32701  dmdsl3  32704  mdexchi  32724  cvexchlem  32757  atcv1  32769  atcvatlem  32774  atabsi  32790  mdsymlem2  32793  mdsymlem5  32796  sumdmdii  32804  sumdmdlem  32807  sumdmdlem2  32808  dya2iocnrect  34703  bnj571  35326  pconnconn  35744  iccllysconn  35763  satffunlem2lem1  35917  cgrextend  36521  btwnexch2  36536  colineardim1  36574  lineext  36589  btwnconn1lem13  36612  btwnconn1lem14  36613  seglecgr12im  36623  outsideofeq  36643  outsideofeu  36644  nn0prpwlem  36874  neibastop2lem  36912  tailfb  36929  nndivsub  37009  ee7.2aOLD  37013  fvineqsneu  38098  poimirlem31  38343  heicant  38347  filbcmb  38432  prdsbnd2  38487  heibor  38513  rngoisocnv  38673  ax12eq  39756  ax12el  39757  pmodlem2  40662  cdleme22b  41156  cdleme32d  41259  cdleme32f  41261  trlord  41384  cdlemj2  41637  cdlemk38  41730  cdlemk19x  41758  dihord2pre  42040  fsuppind  43363  mzpcompact2lem  43523  pellfundex  43654  acongsym  43744  pwssplit4  43857  pwslnm  43862  cantnfresb  44092  relexpmulg  44477  relpmin  45702  stoweidlem17  46772  2reu8i  47891  imasetpreimafvbijlemf1  48194  iccpartigtl  48213  paireqne  48301  fmtnofac2lem  48361  2pwp1prmfmtno  48383  lighneallem4  48403  bgoldbtbndlem2  48612  bgoldbtbndlem3  48613  bgoldbtbnd  48615  grimco  48695  isuspgrimlem  48701  cycl3grtri  48753  isubgr3stgrlem6  48777  lmod0rng  49035  2zrngamgm  49051