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 φψθχθ

Proof

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