Metamath Proof Explorer


Theorem orbi2d

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

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

Proof

Step Hyp Ref Expression
1 bid.1 φ ψ χ
2 1 imbi2d φ ¬ θ ψ ¬ θ χ
3 df-or θ ψ ¬ θ ψ
4 df-or θ χ ¬ θ χ
5 2 3 4 3bitr4g φ θ ψ θ χ