Metamath Proof Explorer


Theorem anbi1

Description: Introduce a right conjunct to both sides of a logical equivalence. Theorem *4.36 of WhiteheadRussell p. 118. (Contributed by NM, 3-Jan-2005)

Ref Expression
Assertion anbi1 φψφχψχ

Proof

Step Hyp Ref Expression
1 id φψφψ
2 1 anbi1d φψφχψχ