Theorem mp3an23 1363

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 1360	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan2 425	1 |- ( ph -> th )

Syntax hints:   -> wi 4   /\ w3a 1002

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

This theorem depends on definitions:  df-bi 117  df-3an 1004

This theorem is referenced by:  sbciegf  3061  ac6sfi  7080  dju0en  7419  1qec  7598  ltaddnq  7617  halfnqq  7620  1idsr  7978  pn0sr  7981  ltm1sr  7987  muleqadd  8838  halfcl  9360  rehalfcl  9361  half0  9362  2halves  9363  halfpos2  9364  halfnneg2  9366  halfaddsub  9368  nneoor  9572  zeo  9575  fztp  10303  modqfrac  10589  iexpcyc  10896  bcn2  11016  bcpasc  11018  imre  11402  reim  11403  crim  11409  addcj  11442  imval2  11445  sinf  12255  efi4p  12268  resin4p  12269  recos4p  12270  sinneg  12277  efival  12283  cosadd  12288  sinmul  12295  sinbnd  12303  cosbnd  12304  ef01bndlem  12307  sin01bnd  12308  cos01bnd  12309  sin01gt0  12313  cos01gt0  12314  sin02gt0  12315  odd2np1lem  12423  odd2np1  12424  pythagtriplem12  12838  pockthi  12921  opprsubrngg  14215  opprdomnbg  14278  isridl  14508  zlmval  14631  zlmlemg  14632  zlmsca  14636  zlmvscag  14637  mopnex  15219  sub1cncf  15316  sub2cncf  15317  sincosq1lem  15539  sincosq2sgn  15541  sincosq3sgn  15542  sincosq4sgn  15543  sinq12gt0  15544  abssinper  15560  coskpi  15562  rpcxpsqrt  15636  logsqrt  15637  2lgsoddprmlem2  15825