Metamath Proof Explorer

Theorem orbi2i

Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993) (Proof shortened by Wolf Lammen, 12-Dec-2012)

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


Step Hyp Ref Expression
1 orbi2i.1 φ ψ
2 1 biimpi φ ψ
3 2 orim2i χ φ χ ψ
4 1 biimpri ψ φ
5 4 orim2i χ ψ χ φ
6 3 5 impbii χ φ χ ψ