Theorem mp3an13 1328

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

Syntax hints:   -> wi 4   /\ w3a 978

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 980

This theorem is referenced by:  pitonnlem1p1  7848  mulrid  7957  addltmul  9158  eluzaddi  9557  fz01en  10056  fznatpl1  10079  expubnd  10580  bernneq  10644  bernneq2  10645  efi4p  11728  efival  11743  cos2tsin  11762  cos01bnd  11769  cos01gt0  11773  dvds0  11816  odd2np1  11881  opoe  11903  gcdid  11990  pythagtriplem4  12271  fvpr0o  12766  fvpr1o  12767  blssioo  14185  tgioo  14186  rerestcntop  14190  sinperlem  14369  sincosq1sgn  14387  sincosq2sgn  14388  sinq12gt0  14391  cosq14gt0  14393