Metamath Proof Explorer

Theorem simpll

Description: Simplification of a conjunction. (Contributed by NM, 18-Mar-2007)

Ref Expression
Assertion simpll 
|- ( ( ( ph /\ ps ) /\ ch ) -> ph )

Proof

Step Hyp Ref Expression
1 id 
 |-  ( ph -> ph )
2 1 ad2antrr 
 |-  ( ( ( ph /\ ps ) /\ ch ) -> ph )