Metamath Proof Explorer


Theorem e01an

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

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

Proof

Step Hyp Ref Expression
1 e01an.1
 |-  ph
2 e01an.2
 |-  (. ps ->. ch ).
3 e01an.3
 |-  ( ( ph /\ ch ) -> th )
4 3 ex
 |-  ( ph -> ( ch -> th ) )
5 1 2 4 e01
 |-  (. ps ->. th ).