Metamath Proof Explorer

Theorem imbi1i

Description: Introduce a consequent to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 17-Sep-2013)

Ref Expression
Hypothesis imbi1i.1 φ ψ
Assertion imbi1i φ χ ψ χ


Step Hyp Ref Expression
1 imbi1i.1 φ ψ
2 imbi1 φ ψ φ χ ψ χ
3 1 2 ax-mp φ χ ψ χ