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  7130  pitonnlem1p1  8056  mulrid  8166  addltmul  9371  eluzaddi  9773  fz01en  10278  fznatpl1  10301  expubnd  10848  bernneq  10912  bernneq2  10913  efi4p  12268  efival  12283  cos2tsin  12302  cos01bnd  12309  cos01gt0  12314  dvds0  12357  odd2np1  12424  opoe  12446  gcdid  12547  pythagtriplem4  12831  fvpr0o  13414  fvpr1o  13415  blssioo  15267  tgioo  15268  rerestcntop  15272  rerest  15274  sinperlem  15522  sincosq1sgn  15540  sincosq2sgn  15541  sinq12gt0  15544  cosq14gt0  15546  1sgmprm  15708