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


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