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

Metamath Proof Explorer

Theorem orbi1r

Description: orbi1 with order of disjuncts reversed. Derived from orbi1rVD . (Contributed by Alan Sare, 31-Dec-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion orbi1r ⊢ φ ↔ ψ → χ ∨ φ ↔ χ ∨ ψ

Proof

Step Hyp Ref Expression
1 id ⊢ φ ↔ ψ → φ ↔ ψ
2 1 orbi2d ⊢ φ ↔ ψ → χ ∨ φ ↔ χ ∨ ψ