Theorem mp3an13 1306

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

Syntax hints:   -> wi 4   /\ w3a 962

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 964

This theorem is referenced by:  pitonnlem1p1  7654  mulid1  7763  addltmul  8956  eluzaddi  9352  fz01en  9833  fznatpl1  9856  expubnd  10350  bernneq  10412  bernneq2  10413  efi4p  11424  efival  11439  cos2tsin  11458  cos01bnd  11465  cos01gt0  11469  dvds0  11508  odd2np1  11570  opoe  11592  gcdid  11674  blssioo  12714  tgioo  12715  rerestcntop  12719  sinperlem  12889  sincosq1sgn  12907  sincosq2sgn  12908  sinq12gt0  12911  cosq14gt0  12913