Theorem mp3an13 1369

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

Syntax hints:   -> wi 4   /\ w3a 1009

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 1011

This theorem is referenced by:  residfi  7244  pitonnlem1p1  8203  mulrid  8313  addltmul  9521  eluzaddi  9928  fz01en  10437  fznatpl1  10461  expubnd  11011  bernneq  11076  bernneq2  11077  efi4p  12462  efival  12477  cos2tsin  12496  cos01bnd  12503  cos01gt0  12508  dvds0  12551  odd2np1  12618  opoe  12640  gcdid  12741  pythagtriplem4  13025  fvpr0o  13639  fvpr1o  13640  blssioo  15577  tgioo  15578  rerestcntop  15582  rerest  15584  sinperlem  15832  sincosq1sgn  15850  sincosq2sgn  15851  sinq12gt0  15854  cosq14gt0  15856  1sgmprm  16022  konigsberg  16648