Theorem mp3an13 1362

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

Syntax hints:   -> wi 4   /\ w3a 1002

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 1004

This theorem is referenced by:  residfi  7107  pitonnlem1p1  8033  mulrid  8143  addltmul  9348  eluzaddi  9749  fz01en  10249  fznatpl1  10272  expubnd  10818  bernneq  10882  bernneq2  10883  efi4p  12228  efival  12243  cos2tsin  12262  cos01bnd  12269  cos01gt0  12274  dvds0  12317  odd2np1  12384  opoe  12406  gcdid  12507  pythagtriplem4  12791  fvpr0o  13374  fvpr1o  13375  blssioo  15227  tgioo  15228  rerestcntop  15232  rerest  15234  sinperlem  15482  sincosq1sgn  15500  sincosq2sgn  15501  sinq12gt0  15504  cosq14gt0  15506  1sgmprm  15668