Metamath Proof Explorer


Theorem eelT1

Description: Syllogism inference combined with modus ponens. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Alan Sare, 23-Dec-2016) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses eelT1.1
|- ( T. -> ph )
eelT1.2
|- ( ps -> ch )
eelT1.3
|- ( ( ph /\ ch ) -> th )
Assertion eelT1
|- ( ps -> th )

Proof

Step Hyp Ref Expression
1 eelT1.1
 |-  ( T. -> ph )
2 eelT1.2
 |-  ( ps -> ch )
3 eelT1.3
 |-  ( ( ph /\ ch ) -> th )
4 1 mptru
 |-  ph
5 4 2 3 sylancr
 |-  ( ps -> th )