Theorem mp3anl2 908

Description: An inference based on modus ponens.

Hypotheses

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

Assertion

Ref	Expression
mp3anl2	|- (((ph /\ ch) /\ th) -> ta)

Proof of Theorem mp3anl2

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

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

This theorem is referenced by:  mp3anr2 911  recp1lt1 5849  climmullem4 7059  geoisumr 7178  efcltlem1 7246  lmuni 7886  metelcls 7900  nvlmle 8268  htthlem6 8555  bcs2t 8970  occllem6 9094  nmopub2tALT 9750  nmfnleub2t 9766  nmopco 9942  nmopcoadj 9948  atord 10219  mdsymlem5 10242

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 775

Copyright terms: Public domain