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 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  3827  predeq1  6323  wrecseq1  8343  ac6sfi  9320  unfilem1  9343  fiint  9366  ordtypelem2  9559  infxpenc2  10062  dju0en  10216  cfsmolem  10310  axdc4lem  10495  1nqenq  11002  mul02lem1  11437  muleqadd  11907  halfcl  12491  rehalfcl  12492  half0  12493  2halves  12494  halfpos2  12495  halfnneg2  12497  halfaddsub  12499  nneo  12702  zeo  12704  peano5uzi  12707  fztp  13620  uzrdgxfr  14008  bcn2  14358  bcpasc  14360  hashxplem  14472  hashfun  14476  swrds2  14979  repsw2  14989  repsw3  14990  imre  15147  reim  15148  crim  15154  addcj  15187  imval2  15190  cnpart  15279  01sqrexlem7  15287  absmax  15368  binomfallfaclem2  16076  bpoly2  16093  bpoly3  16094  fsumcube  16096  efgt0  16139  sinf  16160  efi4p  16173  resin4p  16174  recos4p  16175  sinneg  16182  efival  16188  cosadd  16201  sinmul  16208  sinbnd  16216  cosbnd  16217  ef01bndlem  16220  sin01bnd  16221  cos01bnd  16222  sin01gt0  16226  cos01gt0  16227  sin02gt0  16228  rpnnen2lem11  16260  rpnnen2lem12  16261  odd2np1lem  16377  odd2np1  16378  pythagtriplem12  16864  pythagtriplem14  16866  pythagtriplem15  16867  pythagtriplem16  16868  pythagtriplem17  16869  pockthi  16945  prmreclem5  16958  prmreclem6  16959  prmlem0  17143  prdsplusg  17503  prdsmulr  17504  prdsvsca  17505  isghm  19233  odinf  19581  lbsexg  21166  psgnghm2  21599  mopnex  24532  tngnm  24672  tngngp2  24673  tngngpd  24674  tngngp  24675  addccncf  24943  sub1cncf  24945  sub2cncf  24946  iihalf1  24958  iihalf2  24961  pjthlem1  25471  ovolunlem1a  25531  ovolunlem1  25532  opnmbllem  25636  vitalilem4  25646  iblcnlem1  25823  itgcnlem  25825  dvmptre  26007  dvmptim  26008  dvlipcn  26033  mdegldg  26105  aaliou3lem3  26386  aaliou3lem8  26387  sincosq1lem  26539  sincosq2sgn  26541  sincosq3sgn  26542  sincosq4sgn  26543  sinq12gt0  26549  abssinper  26563  coskpi  26565  sineq0  26566  coseq1  26567  efeq1  26570  resinf1o  26578  efif1olem2  26585  efif1olem4  26587  logneg2  26657  cxpsqrtlem  26744  cxpsqrt  26745  logsqrt  26746  1cubr  26885  leibpilem2  26984  basellem3  27126  ppiub  27248  chtublem  27255  chtub  27256  bcmax  27322  bcp1ctr  27323  bposlem2  27329  bposlem6  27333  bposlem9  27336  logdivsum  27577  elno  27690  mulscl  28160  4ipval2  30727  ipidsq  30729  dipcl  30731  dipcj  30733  ipasslem11  30859  hvmul0  31043  pjhthlem1  31410  h1de2bi  31573  spanunsni  31598  adjeu  31908  nmopge0  31930  nmfnge0  31946  opsqrlem6  32164  mdsl1i  32340  mdsl2bi  32342  mdexchi  32354  superpos  32373  atabsi  32420  dmdbr5ati  32441  cdj3lem1  32453  fpwrelmapffslem  32743  dp2cl  32862  dpfrac1  32874  cshw1s2  32945  ogrpaddlt  33094  ofldlt1  33343  ofldchr  33344  oddpwdc  34356  eulerpartgbij  34374  subfacp1lem2a  35185  subfacp1lem5  35189  subfacp1lem6  35190  subfaclim  35193  sinccvglem  35677  dfon2lem3  35786  dfon2lem7  35790  wsuceq1  35816  clsun  36329  vtoclefex  37335  finxpreclem5  37396  sin2h  37617  cos2h  37618  tan2h  37619  poimirlem22  37649  poimirlem31  37658  opnmbllem0  37663  mblfinlem3  37666  itg2addnclem3  37680  ftc1cnnclem  37698  ftc1anclem6  37705  ftc2nc  37709  dvasin  37711  fdc  37752  constcncf  37769  heiborlem7  37824  atlatmstc  39320  lcmineqlem10  42039  lcmineqlem12  42041  facp2  42144  fac2xp3  42240  sn-00idlem1  42428  0prjspnlem  42633  sn-isghm  42683  diophren  42824  oaabsb  43307  dftrcl3  43733  dfrtrcl3  43746  cotrclrcl  43755  lhe4.4ex1a  44348  dirkerper  46111  zlmodzxznm  48414  sinh-conventional  49258