Theorem mp3an23 1260

Description: An inference based on modus ponens. (Contributed by NM, 14-Jul-2005.)

Hypotheses

Ref	Expression
mp3an23.1	|- ps
mp3an23.2	|- ch
mp3an23.3	|- ( ( ph /\ ps /\ ch ) -> th )

Assertion

Ref	Expression
mp3an23	|- ( ph -> th )

Proof of Theorem mp3an23

Step	Hyp	Ref	Expression
1		mp3an23.1	. 2 |- ps
2		mp3an23.2	. . 3 |- ch
3		mp3an23.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1257	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 415	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 919

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem depends on definitions:  df-bi 115  df-3an 921

This theorem is referenced by:  sbciegf  2845  ac6sfi  6379  1qec  6578  ltaddnq  6597  halfnqq  6600  1idsr  6945  pn0sr  6948  muleqadd  7758  halfcl  8257  rehalfcl  8258  half0  8259  2halves  8260  halfpos2  8261  halfnneg2  8263  halfaddsub  8265  nneoor  8449  zeo  8452  fztp  9095  modqfrac  9339  iexpcyc  9579  bcn2  9691  bcpasc  9693  imre  9738  reim  9739  crim  9745  addcj  9778  imval2  9781  odd2np1lem  10271  odd2np1  10272