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 ( 𝜑 → ( ( 𝜓𝜃 ) ↔ ( 𝜒𝜃 ) ) )