Theorem orbi12i 765

Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12i.1	⊢ (𝜑 ↔ 𝜓)
orbi12i.2	⊢ (𝜒 ↔ 𝜃)

Assertion

Ref	Expression
orbi12i	⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 ⊢ (𝜒 ↔ 𝜃)
2	1	orbi2i 763	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 764	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 184	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 105   ∨ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  820  anddi  822  3orbi123i  1191  3or6  1335  excxor  1397  19.33b2  1651  sbequilem  1860  sborv  1913  sbor  1981  r19.43  2663  rexun  3352  indi  3419  difindiss  3426  symdifxor  3438  unab  3439  dfpr2  3651  rabrsndc  3700  pwprss  3845  pwtpss  3846  unipr  3863  uniun  3868  iunun  4005  iunxun  4006  brun  4094  pwunss  4329  ordsoexmid  4609  onintexmid  4620  dcextest  4628  opthprc  4725  cnvsom  5225  ftpg  5767  tpostpos  6349  eldju  7169  djur  7170  ltexprlemloc  7719  axpre-ltwlin  7995  axpre-apti  7997  axpre-mulext  8000  axpre-suploc  8014  fz01or  10232  cbvsum  11642  fsum3  11669  cbvprod  11840  fprodseq  11865  gcdsupex  12249  gcdsupcl  12250  pythagtriplem2  12560  pythagtrip  12577