Metamath Proof Explorer


Theorem e22an

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

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

Proof

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