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  7254  pitonnlem1p1  8213  mulrid  8323  addltmul  9542  eluzaddi  9949  fz01en  10459  fznatpl1  10483  expubnd  11033  bernneq  11098  bernneq2  11099  efi4p  12484  efival  12499  cos2tsin  12518  cos01bnd  12525  cos01gt0  12530  dvds0  12573  odd2np1  12640  opoe  12662  gcdid  12763  pythagtriplem4  13047  fvpr0o  13662  fvpr1o  13663  blssioo  15654  tgioo  15655  rerestcntop  15659  rerest  15661  sinperlem  15909  sincosq1sgn  15927  sincosq2sgn  15928  sinq12gt0  15931  cosq14gt0  15933  1sgmprm  16108  konigsberg  16734