Theorem mp3an13 907

Description: An inference based on modus ponens.

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

Syntax hints:   -> wi 3   /\ w3a 775

This theorem is referenced by:  nneob 4255  negeu 5355  receu 5701  nnleltp1t 5954  nnaddm1clt 5958  elnn0nn 6171  dfuz 6202  uzindOLD 6208  seq1lem2 6310  eluzaddi 6436  expubndt 6608  bernneq 6652  bernneq2 6653  discrlem3 6658  facwordit 6944  climubi 7153  geolimilem 7235  0.999... 7246  cvgratlem1ALT 7247  erelem3 7321  efaddlem1 7338  efaddlem14 7351  efaddlem15 7352  efaddlem16 7353  ef1tllem 7381  eflegeolem1 7413  efi4pt 7435  efivalt 7447  sin01bndlem3 7469  cos01gt0 7477  bcthlem1 7999  bcthlem8 8006  sm1cnilem 8347  ipid 8363  ip1cnilem1 8373  ip1cnilem2 8374  ip1cnilem3 8375  ip1cnilem5 8377  ip1cnilem6 8378  ipasslem1 8490  ipasslem2 8491  ipasslem4 8493  ipasslem5 8494  ipasslem6 8495  ipasslem8 8497  ipasslem9 8498  ipasslem11 8500  minveclem27 8571  sincosq1sgn 8704  sincosq2sgn 8705  sinq12gt0t 8708  cosh111lem1 8714  efper 8747  pjthlem14 9232  chrelat 10291  chrelat2 10292  cvexchlem 10295  cayleylem3 10411

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225  df-3an 777

Copyright terms: Public domain