Theorem mp3an23 1456

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 1453	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)
5	1, 4	mpan2 692	1 ⊢ (𝜑 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  sbciegf  3763  predeq1  6256  wrecseq1  8254  ac6sfi  9183  unfilem1  9204  fiint  9226  ordtypelem2  9423  infxpenc2  9933  dju0en  10087  cfsmolem  10181  axdc4lem  10366  1nqenq  10874  mul02lem1  11311  muleqadd  11783  2halves  12384  halfcl  12392  rehalfcl  12393  half0  12394  halfpos2  12395  halfnneg2  12397  halfaddsub  12399  nneo  12602  zeo  12604  peano5uzi  12607  fztp  13523  uzrdgxfr  13918  bcn2  14270  bcpasc  14272  hashxplem  14384  hashfun  14388  swrds2  14891  repsw2  14901  repsw3  14902  imre  15059  reim  15060  crim  15066  addcj  15099  imval2  15102  cnpart  15191  01sqrexlem7  15199  absmax  15281  binomfallfaclem2  15994  bpoly2  16011  bpoly3  16012  fsumcube  16014  efgt0  16059  sinf  16080  efi4p  16093  resin4p  16094  recos4p  16095  sinneg  16102  efival  16108  cosadd  16121  sinmul  16128  sinbnd  16136  cosbnd  16137  ef01bndlem  16140  sin01bnd  16141  cos01bnd  16142  sin01gt0  16146  cos01gt0  16147  sin02gt0  16148  rpnnen2lem11  16180  rpnnen2lem12  16181  odd2np1lem  16298  odd2np1  16299  pythagtriplem12  16786  pythagtriplem14  16788  pythagtriplem15  16789  pythagtriplem16  16790  pythagtriplem17  16791  pockthi  16867  prmreclem5  16880  prmreclem6  16881  prmlem0  17065  prdsplusg  17410  prdsmulr  17411  prdsvsca  17412  isghm  19179  odinf  19527  ogrpaddlt  20102  ofldlt1  20841  lbsexg  21151  ofldchr  21545  psgnghm2  21550  mopnex  24472  tngnm  24604  tngngp2  24605  tngngpd  24606  tngngp  24607  addccncf  24872  sub1cncf  24874  sub2cncf  24875  iihalf1  24886  iihalf2  24888  pjthlem1  25392  ovolunlem1a  25451  ovolunlem1  25452  opnmbllem  25556  vitalilem4  25566  iblcnlem1  25743  itgcnlem  25745  dvmptre  25924  dvmptim  25925  dvlipcn  25949  mdegldg  26019  aaliou3lem3  26298  aaliou3lem8  26299  sincosq1lem  26449  sincosq2sgn  26451  sincosq3sgn  26452  sincosq4sgn  26453  sinq12gt0  26459  abssinper  26473  coskpi  26475  sineq0  26476  coseq1  26477  efeq1  26480  resinf1o  26488  efif1olem2  26495  efif1olem4  26497  logneg2  26567  cxpsqrtlem  26654  cxpsqrt  26655  logsqrt  26656  1cubr  26794  leibpilem2  26893  basellem3  27034  ppiub  27155  chtublem  27162  chtub  27163  bcmax  27229  bcp1ctr  27230  bposlem2  27236  bposlem6  27240  bposlem9  27243  logdivsum  27484  elno  27597  mulscl  28114  4ipval2  30767  ipidsq  30769  dipcl  30771  dipcj  30773  ipasslem11  30899  hvmul0  31083  pjhthlem1  31450  h1de2bi  31613  spanunsni  31638  adjeu  31948  nmopge0  31970  nmfnge0  31986  opsqrlem6  32204  mdsl1i  32380  mdsl2bi  32382  mdexchi  32394  superpos  32413  atabsi  32460  dmdbr5ati  32481  cdj3lem1  32493  fpwrelmapffslem  32793  dp2cl  32927  dpfrac1  32939  cshw1s2  33008  oddpwdc  34486  eulerpartgbij  34504  subfacp1lem2a  35350  subfacp1lem5  35354  subfacp1lem6  35355  subfaclim  35358  sinccvglem  35842  dfon2lem3  35953  dfon2lem7  35957  wsuceq1  35983  clsun  36498  vtoclefex  37638  finxpreclem5  37699  sin2h  37919  cos2h  37920  tan2h  37921  poimirlem22  37951  poimirlem31  37960  opnmbllem0  37965  mblfinlem3  37968  itg2addnclem3  37982  ftc1cnnclem  38000  ftc1anclem6  38007  ftc2nc  38011  dvasin  38013  fdc  38054  constcncf  38071  heiborlem7  38126  atlatmstc  39753  lcmineqlem10  42465  lcmineqlem12  42467  facp2  42570  3rdpwhole  42712  sn-00idlem1  42818  0prjspnlem  43044  sn-isghm  43094  diophren  43229  oaabsb  43710  dftrcl3  44135  dfrtrcl3  44148  cotrclrcl  44157  lhe4.4ex1a  44744  dirkerper  46512  sinnpoly  47327  zlmodzxznm  48961  sinh-conventional  50202