Theorem mp3an13 1339

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 1337	. 2 |- ( ( ph /\ ps ) -> th )
5	1, 4	mpan 424	1 |- ( ps -> th )

Syntax hints:   -> wi 4   /\ w3a 980

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 982

This theorem is referenced by:  residfi  7001  pitonnlem1p1  7908  mulrid  8018  addltmul  9222  eluzaddi  9622  fz01en  10122  fznatpl1  10145  expubnd  10670  bernneq  10734  bernneq2  10735  efi4p  11863  efival  11878  cos2tsin  11897  cos01bnd  11904  cos01gt0  11909  dvds0  11952  odd2np1  12017  opoe  12039  gcdid  12126  pythagtriplem4  12409  fvpr0o  12927  fvpr1o  12928  blssioo  14732  tgioo  14733  rerestcntop  14737  rerest  14739  sinperlem  14984  sincosq1sgn  15002  sincosq2sgn  15003  sinq12gt0  15006  cosq14gt0  15008