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  3781  predeq1  6271  wrecseq1  8269  ac6sfi  9198  unfilem1  9219  fiint  9241  ordtypelem2  9438  infxpenc2  9946  dju0en  10100  cfsmolem  10194  axdc4lem  10379  1nqenq  10887  mul02lem1  11323  muleqadd  11795  2halves  12373  halfcl  12381  rehalfcl  12382  half0  12383  halfpos2  12384  halfnneg2  12386  halfaddsub  12388  nneo  12590  zeo  12592  peano5uzi  12595  fztp  13510  uzrdgxfr  13904  bcn2  14256  bcpasc  14258  hashxplem  14370  hashfun  14374  swrds2  14877  repsw2  14887  repsw3  14888  imre  15045  reim  15046  crim  15052  addcj  15085  imval2  15088  cnpart  15177  01sqrexlem7  15185  absmax  15267  binomfallfaclem2  15977  bpoly2  15994  bpoly3  15995  fsumcube  15997  efgt0  16042  sinf  16063  efi4p  16076  resin4p  16077  recos4p  16078  sinneg  16085  efival  16091  cosadd  16104  sinmul  16111  sinbnd  16119  cosbnd  16120  ef01bndlem  16123  sin01bnd  16124  cos01bnd  16125  sin01gt0  16129  cos01gt0  16130  sin02gt0  16131  rpnnen2lem11  16163  rpnnen2lem12  16164  odd2np1lem  16281  odd2np1  16282  pythagtriplem12  16768  pythagtriplem14  16770  pythagtriplem15  16771  pythagtriplem16  16772  pythagtriplem17  16773  pockthi  16849  prmreclem5  16862  prmreclem6  16863  prmlem0  17047  prdsplusg  17392  prdsmulr  17393  prdsvsca  17394  isghm  19161  odinf  19509  ogrpaddlt  20084  ofldlt1  20825  lbsexg  21136  ofldchr  21548  psgnghm2  21553  mopnex  24480  tngnm  24612  tngngp2  24613  tngngpd  24614  tngngp  24615  addccncf  24883  sub1cncf  24885  sub2cncf  24886  iihalf1  24898  iihalf2  24901  pjthlem1  25410  ovolunlem1a  25470  ovolunlem1  25471  opnmbllem  25575  vitalilem4  25585  iblcnlem1  25762  itgcnlem  25764  dvmptre  25946  dvmptim  25947  dvlipcn  25972  mdegldg  26044  aaliou3lem3  26325  aaliou3lem8  26326  sincosq1lem  26479  sincosq2sgn  26481  sincosq3sgn  26482  sincosq4sgn  26483  sinq12gt0  26489  abssinper  26503  coskpi  26505  sineq0  26506  coseq1  26507  efeq1  26510  resinf1o  26518  efif1olem2  26525  efif1olem4  26527  logneg2  26597  cxpsqrtlem  26684  cxpsqrt  26685  logsqrt  26686  1cubr  26825  leibpilem2  26924  basellem3  27066  ppiub  27188  chtublem  27195  chtub  27196  bcmax  27262  bcp1ctr  27263  bposlem2  27269  bposlem6  27273  bposlem9  27276  logdivsum  27517  elno  27630  mulscl  28147  4ipval2  30802  ipidsq  30804  dipcl  30806  dipcj  30808  ipasslem11  30934  hvmul0  31118  pjhthlem1  31485  h1de2bi  31648  spanunsni  31673  adjeu  31983  nmopge0  32005  nmfnge0  32021  opsqrlem6  32239  mdsl1i  32415  mdsl2bi  32417  mdexchi  32429  superpos  32448  atabsi  32495  dmdbr5ati  32516  cdj3lem1  32528  fpwrelmapffslem  32828  dp2cl  32978  dpfrac1  32990  cshw1s2  33059  oddpwdc  34538  eulerpartgbij  34556  subfacp1lem2a  35402  subfacp1lem5  35406  subfacp1lem6  35407  subfaclim  35410  sinccvglem  35894  dfon2lem3  36005  dfon2lem7  36009  wsuceq1  36035  clsun  36550  vtoclefex  37616  finxpreclem5  37677  sin2h  37890  cos2h  37891  tan2h  37892  poimirlem22  37922  poimirlem31  37931  opnmbllem0  37936  mblfinlem3  37939  itg2addnclem3  37953  ftc1cnnclem  37971  ftc1anclem6  37978  ftc2nc  37982  dvasin  37984  fdc  38025  constcncf  38042  heiborlem7  38097  atlatmstc  39724  lcmineqlem10  42437  lcmineqlem12  42439  facp2  42542  3rdpwhole  42691  sn-00idlem1  42797  0prjspnlem  43010  sn-isghm  43060  diophren  43199  oaabsb  43680  dftrcl3  44105  dfrtrcl3  44118  cotrclrcl  44127  lhe4.4ex1a  44714  dirkerper  46483  sinnpoly  47280  zlmodzxznm  48886  sinh-conventional  50127