Theorem mp3an13 1323

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

Syntax hints:   -> wi 4   /\ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  pitonnlem1p1  7808  mulid1  7917  addltmul  9114  eluzaddi  9513  fz01en  10009  fznatpl1  10032  expubnd  10533  bernneq  10596  bernneq2  10597  efi4p  11680  efival  11695  cos2tsin  11714  cos01bnd  11721  cos01gt0  11725  dvds0  11768  odd2np1  11832  opoe  11854  gcdid  11941  pythagtriplem4  12222  blssioo  13339  tgioo  13340  rerestcntop  13344  sinperlem  13523  sincosq1sgn  13541  sincosq2sgn  13542  sinq12gt0  13545  cosq14gt0  13547