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  3794  predeq1  6278  wrecseq1  8296  ac6sfi  9237  unfilem1  9260  fiint  9283  ordtypelem2  9478  infxpenc2  9981  dju0en  10135  cfsmolem  10229  axdc4lem  10414  1nqenq  10921  mul02lem1  11356  muleqadd  11828  2halves  12406  halfcl  12414  rehalfcl  12415  half0  12416  halfpos2  12417  halfnneg2  12419  halfaddsub  12421  nneo  12624  zeo  12626  peano5uzi  12629  fztp  13547  uzrdgxfr  13938  bcn2  14290  bcpasc  14292  hashxplem  14404  hashfun  14408  swrds2  14912  repsw2  14922  repsw3  14923  imre  15080  reim  15081  crim  15087  addcj  15120  imval2  15123  cnpart  15212  01sqrexlem7  15220  absmax  15302  binomfallfaclem2  16012  bpoly2  16029  bpoly3  16030  fsumcube  16032  efgt0  16077  sinf  16098  efi4p  16111  resin4p  16112  recos4p  16113  sinneg  16120  efival  16126  cosadd  16139  sinmul  16146  sinbnd  16154  cosbnd  16155  ef01bndlem  16158  sin01bnd  16159  cos01bnd  16160  sin01gt0  16164  cos01gt0  16165  sin02gt0  16166  rpnnen2lem11  16198  rpnnen2lem12  16199  odd2np1lem  16316  odd2np1  16317  pythagtriplem12  16803  pythagtriplem14  16805  pythagtriplem15  16806  pythagtriplem16  16807  pythagtriplem17  16808  pockthi  16884  prmreclem5  16897  prmreclem6  16898  prmlem0  17082  prdsplusg  17427  prdsmulr  17428  prdsvsca  17429  isghm  19153  odinf  19499  lbsexg  21080  psgnghm2  21496  mopnex  24413  tngnm  24545  tngngp2  24546  tngngpd  24547  tngngp  24548  addccncf  24816  sub1cncf  24818  sub2cncf  24819  iihalf1  24831  iihalf2  24834  pjthlem1  25343  ovolunlem1a  25403  ovolunlem1  25404  opnmbllem  25508  vitalilem4  25518  iblcnlem1  25695  itgcnlem  25697  dvmptre  25879  dvmptim  25880  dvlipcn  25905  mdegldg  25977  aaliou3lem3  26258  aaliou3lem8  26259  sincosq1lem  26412  sincosq2sgn  26414  sincosq3sgn  26415  sincosq4sgn  26416  sinq12gt0  26422  abssinper  26436  coskpi  26438  sineq0  26439  coseq1  26440  efeq1  26443  resinf1o  26451  efif1olem2  26458  efif1olem4  26460  logneg2  26530  cxpsqrtlem  26617  cxpsqrt  26618  logsqrt  26619  1cubr  26758  leibpilem2  26857  basellem3  26999  ppiub  27121  chtublem  27128  chtub  27129  bcmax  27195  bcp1ctr  27196  bposlem2  27202  bposlem6  27206  bposlem9  27209  logdivsum  27450  elno  27563  mulscl  28043  4ipval2  30643  ipidsq  30645  dipcl  30647  dipcj  30649  ipasslem11  30775  hvmul0  30959  pjhthlem1  31326  h1de2bi  31489  spanunsni  31514  adjeu  31824  nmopge0  31846  nmfnge0  31862  opsqrlem6  32080  mdsl1i  32256  mdsl2bi  32258  mdexchi  32270  superpos  32289  atabsi  32336  dmdbr5ati  32357  cdj3lem1  32369  fpwrelmapffslem  32661  dp2cl  32806  dpfrac1  32818  cshw1s2  32888  ogrpaddlt  33037  ofldlt1  33297  ofldchr  33298  oddpwdc  34351  eulerpartgbij  34369  subfacp1lem2a  35167  subfacp1lem5  35171  subfacp1lem6  35172  subfaclim  35175  sinccvglem  35659  dfon2lem3  35768  dfon2lem7  35772  wsuceq1  35798  clsun  36311  vtoclefex  37317  finxpreclem5  37378  sin2h  37599  cos2h  37600  tan2h  37601  poimirlem22  37631  poimirlem31  37640  opnmbllem0  37645  mblfinlem3  37648  itg2addnclem3  37662  ftc1cnnclem  37680  ftc1anclem6  37687  ftc2nc  37691  dvasin  37693  fdc  37734  constcncf  37751  heiborlem7  37806  atlatmstc  39307  lcmineqlem10  42021  lcmineqlem12  42023  facp2  42126  3rdpwhole  42275  sn-00idlem1  42381  0prjspnlem  42604  sn-isghm  42654  diophren  42794  oaabsb  43276  dftrcl3  43702  dfrtrcl3  43715  cotrclrcl  43724  lhe4.4ex1a  44311  dirkerper  46087  zlmodzxznm  48476  sinh-conventional  49705