Theorem mp3an13 1364

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

Hypotheses

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

Assertion

Ref	Expression
mp3an13	|- ( ps -> th )

Proof of Theorem mp3an13

Step	Hyp	Ref	Expression
1		mp3an13.1	. 2 |- ph
2		mp3an13.2	. . 3 |- ch
3		mp3an13.3	. . 3 |- ( ( ph /\ ps /\ ch ) -> th )
4	2, 3	mp3an3 1362	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan 424	1 |- ( ps -> th )

Syntax hints:   -> wi 4   /\ w3a 1004

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 1006

This theorem is referenced by:  residfi  7138  pitonnlem1p1  8065  mulrid  8175  addltmul  9380  eluzaddi  9782  fz01en  10287  fznatpl1  10310  expubnd  10857  bernneq  10921  bernneq2  10922  efi4p  12277  efival  12292  cos2tsin  12311  cos01bnd  12318  cos01gt0  12323  dvds0  12366  odd2np1  12433  opoe  12455  gcdid  12556  pythagtriplem4  12840  fvpr0o  13423  fvpr1o  13424  blssioo  15276  tgioo  15277  rerestcntop  15281  rerest  15283  sinperlem  15531  sincosq1sgn  15549  sincosq2sgn  15550  sinq12gt0  15553  cosq14gt0  15555  1sgmprm  15717