Theorem mp3an23 1452

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	⊢ 𝜓
mp3an23.2	⊢ 𝜒
mp3an23.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an23	⊢ (𝜑 → 𝜃)

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 ⊢ 𝜓
2		mp3an23.2	. . 3 ⊢ 𝜒
3		mp3an23.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an3 1449	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 688	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1086

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 397  df-3an 1088

This theorem is referenced by:  sbciegf  3756  predeq1  6208  wrecseq1  8143  ac6sfi  9067  unfilem1  9087  ordtypelem2  9287  infxpenc2  9787  dju0en  9940  cfsmolem  10035  axdc4lem  10220  1nqenq  10727  mul02lem1  11160  muleqadd  11628  halfcl  12207  rehalfcl  12208  half0  12209  2halves  12210  halfpos2  12211  halfnneg2  12213  halfaddsub  12215  nneo  12413  zeo  12415  peano5uzi  12418  fztp  13321  uzrdgxfr  13696  bcn2  14042  bcpasc  14044  hashxplem  14157  hashfun  14161  swrds2  14662  repsw2  14672  repsw3  14673  imre  14828  reim  14829  crim  14835  addcj  14868  imval2  14871  cnpart  14960  sqrlem7  14969  absmax  15050  binomfallfaclem2  15759  bpoly2  15776  bpoly3  15777  fsumcube  15779  efgt0  15821  sinf  15842  efi4p  15855  resin4p  15856  recos4p  15857  sinneg  15864  efival  15870  cosadd  15883  sinmul  15890  sinbnd  15898  cosbnd  15899  ef01bndlem  15902  sin01bnd  15903  cos01bnd  15904  sin01gt0  15908  cos01gt0  15909  sin02gt0  15910  rpnnen2lem11  15942  rpnnen2lem12  15943  odd2np1lem  16058  odd2np1  16059  pythagtriplem12  16536  pythagtriplem14  16538  pythagtriplem15  16539  pythagtriplem16  16540  pythagtriplem17  16541  pockthi  16617  prmreclem5  16630  prmreclem6  16631  prmlem0  16816  prdsplusg  17178  prdsmulr  17179  prdsvsca  17180  odinf  19179  lbsexg  20435  psgnghm2  20795  mopnex  23684  tngnm  23824  tngngp2  23825  tngngpd  23826  tngngp  23827  addccncf  24089  sub1cncf  24091  sub2cncf  24092  iihalf1  24103  iihalf2  24105  pjthlem1  24610  ovolunlem1a  24669  ovolunlem1  24670  opnmbllem  24774  vitalilem4  24784  iblcnlem1  24961  itgcnlem  24963  dvmptre  25142  dvmptim  25143  dvlipcn  25167  mdegldg  25240  aaliou3lem3  25513  aaliou3lem8  25514  sincosq1lem  25663  sincosq2sgn  25665  sincosq3sgn  25666  sincosq4sgn  25667  sinq12gt0  25673  abssinper  25686  coskpi  25688  sineq0  25689  coseq1  25690  efeq1  25693  resinf1o  25701  efif1olem2  25708  efif1olem4  25710  logneg2  25779  cxpsqrtlem  25866  cxpsqrt  25867  logsqrt  25868  1cubr  26001  leibpilem2  26100  basellem3  26241  ppiub  26361  chtublem  26368  chtub  26369  bcmax  26435  bcp1ctr  26436  bposlem2  26442  bposlem6  26446  bposlem9  26449  logdivsum  26690  4ipval2  29079  ipidsq  29081  dipcl  29083  dipcj  29085  ipasslem11  29211  hvmul0  29395  pjhthlem1  29762  h1de2bi  29925  spanunsni  29950  adjeu  30260  nmopge0  30282  nmfnge0  30298  opsqrlem6  30516  mdsl1i  30692  mdsl2bi  30694  mdexchi  30706  superpos  30725  atabsi  30772  dmdbr5ati  30793  cdj3lem1  30805  fpwrelmapffslem  31076  dp2cl  31163  dpfrac1  31175  cshw1s2  31241  ogrpaddlt  31352  ofldlt1  31521  ofldchr  31522  oddpwdc  32330  eulerpartgbij  32348  subfacp1lem2a  33151  subfacp1lem5  33155  subfacp1lem6  33156  subfaclim  33159  sinccvglem  33639  dfon2lem3  33770  dfon2lem7  33774  wsuceq1  33818  clsun  34526  vtoclefex  35514  finxpreclem5  35575  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem22  35808  poimirlem31  35817  opnmbllem0  35822  mblfinlem3  35825  itg2addnclem3  35839  ftc1cnnclem  35857  ftc1anclem6  35864  ftc2nc  35868  dvasin  35870  fdc  35912  constcncf  35929  heiborlem7  35984  atlatmstc  37340  lcmineqlem10  40053  lcmineqlem12  40055  facp2  40106  fac2xp3  40167  sn-00idlem1  40388  0prjspnlem  40467  diophren  40642  dftrcl3  41335  dfrtrcl3  41348  cotrclrcl  41357  lhe4.4ex1a  41954  dirkerper  43644  zlmodzxznm  45849  sinh-conventional  46452