Theorem mp3an23 1455

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 1452	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 691	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  sbciegf  3792  predeq1  6276  wrecseq1  8294  ac6sfi  9231  unfilem1  9254  fiint  9277  ordtypelem2  9472  infxpenc2  9975  dju0en  10129  cfsmolem  10223  axdc4lem  10408  1nqenq  10915  mul02lem1  11350  muleqadd  11822  2halves  12400  halfcl  12408  rehalfcl  12409  half0  12410  halfpos2  12411  halfnneg2  12413  halfaddsub  12415  nneo  12618  zeo  12620  peano5uzi  12623  fztp  13541  uzrdgxfr  13932  bcn2  14284  bcpasc  14286  hashxplem  14398  hashfun  14402  swrds2  14906  repsw2  14916  repsw3  14917  imre  15074  reim  15075  crim  15081  addcj  15114  imval2  15117  cnpart  15206  01sqrexlem7  15214  absmax  15296  binomfallfaclem2  16006  bpoly2  16023  bpoly3  16024  fsumcube  16026  efgt0  16071  sinf  16092  efi4p  16105  resin4p  16106  recos4p  16107  sinneg  16114  efival  16120  cosadd  16133  sinmul  16140  sinbnd  16148  cosbnd  16149  ef01bndlem  16152  sin01bnd  16153  cos01bnd  16154  sin01gt0  16158  cos01gt0  16159  sin02gt0  16160  rpnnen2lem11  16192  rpnnen2lem12  16193  odd2np1lem  16310  odd2np1  16311  pythagtriplem12  16797  pythagtriplem14  16799  pythagtriplem15  16800  pythagtriplem16  16801  pythagtriplem17  16802  pockthi  16878  prmreclem5  16891  prmreclem6  16892  prmlem0  17076  prdsplusg  17421  prdsmulr  17422  prdsvsca  17423  isghm  19147  odinf  19493  lbsexg  21074  psgnghm2  21490  mopnex  24407  tngnm  24539  tngngp2  24540  tngngpd  24541  tngngp  24542  addccncf  24810  sub1cncf  24812  sub2cncf  24813  iihalf1  24825  iihalf2  24828  pjthlem1  25337  ovolunlem1a  25397  ovolunlem1  25398  opnmbllem  25502  vitalilem4  25512  iblcnlem1  25689  itgcnlem  25691  dvmptre  25873  dvmptim  25874  dvlipcn  25899  mdegldg  25971  aaliou3lem3  26252  aaliou3lem8  26253  sincosq1lem  26406  sincosq2sgn  26408  sincosq3sgn  26409  sincosq4sgn  26410  sinq12gt0  26416  abssinper  26430  coskpi  26432  sineq0  26433  coseq1  26434  efeq1  26437  resinf1o  26445  efif1olem2  26452  efif1olem4  26454  logneg2  26524  cxpsqrtlem  26611  cxpsqrt  26612  logsqrt  26613  1cubr  26752  leibpilem2  26851  basellem3  26993  ppiub  27115  chtublem  27122  chtub  27123  bcmax  27189  bcp1ctr  27190  bposlem2  27196  bposlem6  27200  bposlem9  27203  logdivsum  27444  elno  27557  mulscl  28037  4ipval2  30637  ipidsq  30639  dipcl  30641  dipcj  30643  ipasslem11  30769  hvmul0  30953  pjhthlem1  31320  h1de2bi  31483  spanunsni  31508  adjeu  31818  nmopge0  31840  nmfnge0  31856  opsqrlem6  32074  mdsl1i  32250  mdsl2bi  32252  mdexchi  32264  superpos  32283  atabsi  32330  dmdbr5ati  32351  cdj3lem1  32363  fpwrelmapffslem  32655  dp2cl  32800  dpfrac1  32812  cshw1s2  32882  ogrpaddlt  33031  ofldlt1  33291  ofldchr  33292  oddpwdc  34345  eulerpartgbij  34363  subfacp1lem2a  35167  subfacp1lem5  35171  subfacp1lem6  35172  subfaclim  35175  sinccvglem  35659  dfon2lem3  35773  dfon2lem7  35777  wsuceq1  35803  clsun  36316  vtoclefex  37322  finxpreclem5  37383  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem22  37636  poimirlem31  37645  opnmbllem0  37650  mblfinlem3  37653  itg2addnclem3  37667  ftc1cnnclem  37685  ftc1anclem6  37692  ftc2nc  37696  dvasin  37698  fdc  37739  constcncf  37756  heiborlem7  37811  atlatmstc  39312  lcmineqlem10  42026  lcmineqlem12  42028  facp2  42131  3rdpwhole  42280  sn-00idlem1  42386  0prjspnlem  42611  sn-isghm  42661  diophren  42801  oaabsb  43283  dftrcl3  43709  dfrtrcl3  43722  cotrclrcl  43731  lhe4.4ex1a  44318  dirkerper  46094  sinnpoly  46892  zlmodzxznm  48486  sinh-conventional  49728