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 φ ψ χ ψ

Proof

Step Hyp Ref Expression
1 rp-simp2-frege φ ψ χ ψ
2 1 3imp φ ψ χ ψ