Theorem orbi2d 617

Description: Deduction adding a left disjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bid.1	⊢ (φ → (ψ ↔ χ))

Assertion

Ref	Expression
orbi2d	⊢ (φ → ((θ ⋁ ψ) ↔ (θ ⋁ χ)))

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (φ → (ψ ↔ χ))
2	1	imbi2d 615	. 2 ⊢ (φ → ((¬ θ → ψ) ↔ (¬ θ → χ)))
3		df-or 224	. 2 ⊢ ((θ ⋁ ψ) ↔ (¬ θ → ψ))
4		df-or 224	. 2 ⊢ ((θ ⋁ χ) ↔ (¬ θ → χ))
5	2, 3, 4	3bitr4g 558	1 ⊢ (φ → ((θ ⋁ ψ) ↔ (θ ⋁ χ)))

Syntax hints:  ¬ wn 2   → wi 3   ↔ wb 146   ⋁ wo 222

This theorem is referenced by:  orbi1d 618  orbi12d 630  orbidi 747  eueq2 1925  eueq3 1926  sbc2or 1966  ifeq2 2375  elsucg 3050  elsuc2g 3051  ordtri2or 3091  ltsopi 5029  suplem2pr 5175  axlttri 5516  mul0ort 5709  elznn0 6155  elznn 6156  zltp1let 6187  snunioolem 6364  infpn2 7524  sinperlem2 8694

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain