Theorem orbi12i 216

Description: Infer the disjunction of two equivalences.

Hypotheses

Ref	Expression
bi2or.1	⊢ (φ ↔ ψ)
bi2or.2	⊢ (χ ↔ θ)

Assertion

Ref	Expression
orbi12i	⊢ ((φ ∨ χ) ↔ (ψ ∨ θ))

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		bi2or.2	. . 3 ⊢ (χ ↔ θ)
2	1	orbi2i 214	. 2 ⊢ ((φ ∨ χ) ↔ (φ ∨ θ))
3		bi2or.1	. . 3 ⊢ (φ ↔ ψ)
4	3	orbi1i 215	. 2 ⊢ ((φ ∨ θ) ↔ (ψ ∨ θ))
5	2, 4	bitr 151	1 ⊢ ((φ ∨ χ) ↔ (ψ ∨ θ))

Syntax hints:   ↔ wb 127   ∨ wo 195

This theorem is referenced by:  ioran 254  andir 457  anddi 459  xor 500  biass 511  caselem 561  consensus 574  prlem2 577  bi3or 607  19.33b 771  r19.43 1304  sspsstri 1572  indi 1676  symdif2 1690  unab 1691  dfpr2 1821  eltp 1834  zfpair 1891  pwunss 1916  unpr 1930  uniun 1934  iunxun 2035  opthprc 2457  dmun 2536  cnvun 2642  brdom2 3292  kmlem16 3595  ltsor 4055  lesubadd2 4318  leneg 4331  elnn0z 4574  elnn0nn 4593

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

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org