Metamath Proof Explorer

Theorem rp-simp2

Description: Simplification of triple conjunction. Identical to simp2 . (Contributed by RP, 24-Dec-2019) (Proof modification is discouraged.)

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

Proof

Step Hyp Ref Expression
1 rp-simp2-frege 
 |-  ( ph -> ( ps -> ( ch -> ps ) ) )
2 1 3imp 
 |-  ( ( ph /\ ps /\ ch ) -> ps )