Theorem orbi12i 681

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 679	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜑 ∨ 𝜃))
3		orbi12i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
4	3	orbi1i 680	. 2 ⊢ ((𝜑 ∨ 𝜃) ↔ (𝜓 ∨ 𝜃))
5	2, 4	bitri 173	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜃))

Syntax hints:   ↔ wb 98   ∨ wo 629

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  andir  732  anddi  734  dcbii  747  3orbi123i  1094  3or6  1218  excxor  1269  19.33b2  1520  sbequilem  1719  sborv  1770  sbor  1828  r19.43  2468  rexun  3123  indi  3184  difindiss  3191  symdifxor  3203  unab  3204  dfpr2  3394  rabrsndc  3438  pwprss  3576  pwtpss  3577  unipr  3594  uniun  3599  iunun  3734  iunxun  3735  brun  3810  pwunss  4020  ordsoexmid  4286  onintexmid  4297  opthprc  4391  cnvsom  4861  ftpg  5347  tpostpos  5879  ltexprlemloc  6705  axpre-ltwlin  6957  axpre-apti  6959  axpre-mulext  6962