Metamath Proof Explorer

Theorem orbi1d

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993)

Ref Expression
Hypothesis bid.1 φ ψ χ
Assertion orbi1d φ ψ θ χ θ


Step Hyp Ref Expression
1 bid.1 φ ψ χ
2 1 orbi2d φ θ ψ θ χ
3 orcom ψ θ θ ψ
4 orcom χ θ θ χ
5 2 3 4 3bitr4g φ ψ θ χ θ