Theorem mp3anl2 911

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 904	. 2 |- ((ph /\ ch) -> (th -> ta))
5	4	imp 350	1 |- (((ph /\ ch) /\ th) -> ta)

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

This theorem is referenced by:  mp3anr2 914  recp1lt1 5901  climmullem4 7123  geoisumr 7243  efcltlem1 7304  lmuni 7951  metelcls 7965  nvlmle 8333  htthlem6 8625  bcs2t 9049  occllem6 9178  nmopub2tALT 9833  nmfnleub2t 9850  nmopco 10028  nmopcoadj 10034  atord 10311  mdsymlem5 10334

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