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  7220  pitonnlem1p1  8177  mulrid  8287  addltmul  9492  eluzaddi  9899  fz01en  10408  fznatpl1  10432  expubnd  10982  bernneq  11047  bernneq2  11048  efi4p  12428  efival  12443  cos2tsin  12462  cos01bnd  12469  cos01gt0  12474  dvds0  12517  odd2np1  12584  opoe  12606  gcdid  12707  pythagtriplem4  12991  fvpr0o  13605  fvpr1o  13606  blssioo  15544  tgioo  15545  rerestcntop  15549  rerest  15551  sinperlem  15799  sincosq1sgn  15817  sincosq2sgn  15818  sinq12gt0  15821  cosq14gt0  15823  1sgmprm  15988  konigsberg  16614