Theorem orbi12i 754

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

Syntax hints:   ↔ wb 104   ∨ wo 698

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  809  anddi  811  3orbi123i  1179  3or6  1313  excxor  1368  19.33b2  1617  sbequilem  1826  sborv  1878  sbor  1942  r19.43  2624  rexun  3302  indi  3369  difindiss  3376  symdifxor  3388  unab  3389  dfpr2  3595  rabrsndc  3644  pwprss  3785  pwtpss  3786  unipr  3803  uniun  3808  iunun  3944  iunxun  3945  brun  4033  pwunss  4261  ordsoexmid  4539  onintexmid  4550  dcextest  4558  opthprc  4655  cnvsom  5147  ftpg  5669  tpostpos  6232  eldju  7033  djur  7034  ltexprlemloc  7548  axpre-ltwlin  7824  axpre-apti  7826  axpre-mulext  7829  axpre-suploc  7843  fz01or  10046  cbvsum  11301  fsum3  11328  cbvprod  11499  fprodseq  11524  gcdsupex  11890  gcdsupcl  11891  pythagtriplem2  12198  pythagtrip  12215