Metamath Proof Explorer


Theorem e33an

Description: Conjunction form of e33 . (Contributed by Alan Sare, 15-Jun-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypotheses e33an.1
|- (. ph ,. ps ,. ch ->. th ).
e33an.2
|- (. ph ,. ps ,. ch ->. ta ).
e33an.3
|- ( ( th /\ ta ) -> et )
Assertion e33an
|- (. ph ,. ps ,. ch ->. et ).

Proof

Step Hyp Ref Expression
1 e33an.1
 |-  (. ph ,. ps ,. ch ->. th ).
2 e33an.2
 |-  (. ph ,. ps ,. ch ->. ta ).
3 e33an.3
 |-  ( ( th /\ ta ) -> et )
4 3 ex
 |-  ( th -> ( ta -> et ) )
5 1 2 4 e33
 |-  (. ph ,. ps ,. ch ->. et ).