This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem orbi1i

Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993)

Ref Expression
Hypothesis orbi2i.1 ⊢ φ ↔ ψ
Assertion orbi1i ⊢ φ ∨ χ ↔ ψ ∨ χ

Proof

Step Hyp Ref Expression
1 orbi2i.1 ⊢ φ ↔ ψ
2 orcom ⊢ φ ∨ χ ↔ χ ∨ φ
3 1 orbi2i ⊢ χ ∨ φ ↔ χ ∨ ψ
4 orcom ⊢ χ ∨ ψ ↔ ψ ∨ χ
5 2 3 4 3bitri ⊢ φ ∨ χ ↔ ψ ∨ χ