Theorem mp3an13 1365

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

Syntax hints:   -> wi 4   /\ w3a 1005

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 1007

This theorem is referenced by:  residfi  7207  pitonnlem1p1  8161  mulrid  8271  addltmul  9475  eluzaddi  9881  fz01en  10387  fznatpl1  10410  expubnd  10958  bernneq  11022  bernneq2  11023  efi4p  12403  efival  12418  cos2tsin  12437  cos01bnd  12444  cos01gt0  12449  dvds0  12492  odd2np1  12559  opoe  12581  gcdid  12682  pythagtriplem4  12966  fvpr0o  13554  fvpr1o  13555  blssioo  15418  tgioo  15419  rerestcntop  15423  rerest  15425  sinperlem  15673  sincosq1sgn  15691  sincosq2sgn  15692  sinq12gt0  15695  cosq14gt0  15697  1sgmprm  15862  konigsberg  16488