Metamath Proof Explorer

Theorem simprl

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

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

Proof

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