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 )

This proof depends on syntax axioms:   -> wi 4   /\ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  residfi  7258  pitonnlem1p1  8219  mulrid  8329  addltmul  9553  eluzaddi  9965  fz01en  10476  fznatpl1  10500  expubnd  11054  bernneq  11119  bernneq2  11120  efi4p  12509  efival  12524  cos2tsin  12543  cos01bnd  12550  cos01gt0  12555  dvds0  12598  odd2np1  12665  opoe  12687  gcdid  12788  pythagtriplem4  13076  fvpr0o  13721  fvpr1o  13722  blssioo  15779  tgioo  15780  rerestcntop  15784  rerest  15786  sinperlem  16035  sincosq1sgn  16053  sincosq2sgn  16054  sinq12gt0  16057  cosq14gt0  16059  1sgmprm  16288  ppiqub  16293  chtublem  16295  chtqub  16296  bcp1ctr  16306  bpos1lem  16309  bposlem2  16312  bposlem3  16313  bposlem4  16314  bposlem5  16315  bposlem6  16316  bposlem7  16317  bposlem9  16319  konigsberg  16939