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  7015  pitonnlem1p1  7930  mulrid  8040  addltmul  9245  eluzaddi  9645  fz01en  10145  fznatpl1  10168  expubnd  10705  bernneq  10769  bernneq2  10770  efi4p  11899  efival  11914  cos2tsin  11933  cos01bnd  11940  cos01gt0  11945  dvds0  11988  odd2np1  12055  opoe  12077  gcdid  12178  pythagtriplem4  12462  fvpr0o  13043  fvpr1o  13044  blssioo  14873  tgioo  14874  rerestcntop  14878  rerest  14880  sinperlem  15128  sincosq1sgn  15146  sincosq2sgn  15147  sinq12gt0  15150  cosq14gt0  15152  1sgmprm  15314