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  1334  excxor  1389  19.33b2  1643  sbequilem  1852  sborv  1905  sbor  1973  r19.43  2655  rexun  3343  indi  3410  difindiss  3417  symdifxor  3429  unab  3430  dfpr2  3641  rabrsndc  3690  pwprss  3835  pwtpss  3836  unipr  3853  uniun  3858  iunun  3995  iunxun  3996  brun  4084  pwunss  4318  ordsoexmid  4598  onintexmid  4609  dcextest  4617  opthprc  4714  cnvsom  5213  ftpg  5746  tpostpos  6322  eldju  7134  djur  7135  ltexprlemloc  7674  axpre-ltwlin  7950  axpre-apti  7952  axpre-mulext  7955  axpre-suploc  7969  fz01or  10186  cbvsum  11525  fsum3  11552  cbvprod  11723  fprodseq  11748  gcdsupex  12124  gcdsupcl  12125  pythagtriplem2  12435  pythagtrip  12452