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  6999  pitonnlem1p1  7906  mulrid  8016  addltmul  9219  eluzaddi  9619  fz01en  10119  fznatpl1  10142  expubnd  10667  bernneq  10731  bernneq2  10732  efi4p  11860  efival  11875  cos2tsin  11894  cos01bnd  11901  cos01gt0  11906  dvds0  11949  odd2np1  12014  opoe  12036  gcdid  12123  pythagtriplem4  12406  fvpr0o  12924  fvpr1o  12925  blssioo  14713  tgioo  14714  rerestcntop  14718  sinperlem  14943  sincosq1sgn  14961  sincosq2sgn  14962  sinq12gt0  14965  cosq14gt0  14967