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  7006  pitonnlem1p1  7913  mulrid  8023  addltmul  9228  eluzaddi  9628  fz01en  10128  fznatpl1  10151  expubnd  10688  bernneq  10752  bernneq2  10753  efi4p  11882  efival  11897  cos2tsin  11916  cos01bnd  11923  cos01gt0  11928  dvds0  11971  odd2np1  12038  opoe  12060  gcdid  12153  pythagtriplem4  12437  fvpr0o  12984  fvpr1o  12985  blssioo  14789  tgioo  14790  rerestcntop  14794  rerest  14796  sinperlem  15044  sincosq1sgn  15062  sincosq2sgn  15063  sinq12gt0  15066  cosq14gt0  15068  1sgmprm  15230