Theorem mp3anl1 910

Description: An inference based on modus ponens.

Hypotheses

Ref	Expression
mp3anl1.1	|- ph
mp3anl1.2	|- (((ph /\ ps /\ ch) /\ th) -> ta)

Assertion

Ref	Expression
mp3anl1	|- (((ps /\ ch) /\ th) -> ta)

Proof of Theorem mp3anl1

Step	Hyp	Ref	Expression
1		mp3anl1.1	. . 3 |- ph
2		mp3anl1.2	. . . 4 |- (((ph /\ ps /\ ch) /\ th) -> ta)
3	2	ex 373	. . 3 |- ((ph /\ ps /\ ch) -> (th -> ta))
4	1, 3	mp3an1 903	. 2 |- ((ps /\ ch) -> (th -> ta))
5	4	imp 350	1 |- (((ps /\ ch) /\ th) -> ta)

Syntax hints:   -> wi 3   /\ wa 223   /\ w3a 775

This theorem is referenced by:  mp3anr1 913  rec11rt 5779  ltmulgt11t 5846  gt0divt 5853  ge0divt 5854  ledivp1 5906  ltdivp1 5907  qbtwnre 6278  facwordit 6944  facavgt 6955  efaddlem5 7342  methausi 7881  tgioolem 7914  xplmi 7973  xplm 7975  xpcn 7976  bcthlem13 8011  bcthlem14 8012  bcthlem19 8017  bcthlem26 8024  nmobndi 8438  blometi 8463  blocnilem 8464  ubthlem3 8531  ubthlem9 8537  ubthlem10 8538  ubthlem11 8539  mdslmd3 10259  atcvat2 10314  irredlem3 10319  mdsymlem1 10330  cdj1 10360

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