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  7932  mulrid  8042  addltmul  9247  eluzaddi  9647  fz01en  10147  fznatpl1  10170  expubnd  10707  bernneq  10771  bernneq2  10772  efi4p  11901  efival  11916  cos2tsin  11935  cos01bnd  11942  cos01gt0  11947  dvds0  11990  odd2np1  12057  opoe  12079  gcdid  12180  pythagtriplem4  12464  fvpr0o  13045  fvpr1o  13046  blssioo  14897  tgioo  14898  rerestcntop  14902  rerest  14904  sinperlem  15152  sincosq1sgn  15170  sincosq2sgn  15171  sinq12gt0  15174  cosq14gt0  15176  1sgmprm  15338