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  9546  eluzaddi  9958  fz01en  10469  fznatpl1  10493  expubnd  11046  bernneq  11111  bernneq2  11112  efi4p  12500  efival  12515  cos2tsin  12534  cos01bnd  12541  cos01gt0  12546  dvds0  12589  odd2np1  12656  opoe  12678  gcdid  12779  pythagtriplem4  13067  fvpr0o  13711  fvpr1o  13712  blssioo  15703  tgioo  15704  rerestcntop  15708  rerest  15710  sinperlem  15959  sincosq1sgn  15977  sincosq2sgn  15978  sinq12gt0  15981  cosq14gt0  15983  1sgmprm  16189  ppiqub  16194  bcp1ctr  16204  bpos1lem  16207  bposlem2  16210  bposlem3  16211  bposlem4  16212  bposlem5  16213  konigsberg  16832