Theorem orbi12i 759

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

Syntax hints:   ↔ wb 104   ∨ wo 703

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 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  814  anddi  816  3orbi123i  1184  3or6  1318  excxor  1373  19.33b2  1622  sbequilem  1831  sborv  1883  sbor  1947  r19.43  2628  rexun  3307  indi  3374  difindiss  3381  symdifxor  3393  unab  3394  dfpr2  3602  rabrsndc  3651  pwprss  3792  pwtpss  3793  unipr  3810  uniun  3815  iunun  3951  iunxun  3952  brun  4040  pwunss  4268  ordsoexmid  4546  onintexmid  4557  dcextest  4565  opthprc  4662  cnvsom  5154  ftpg  5680  tpostpos  6243  eldju  7045  djur  7046  ltexprlemloc  7569  axpre-ltwlin  7845  axpre-apti  7847  axpre-mulext  7850  axpre-suploc  7864  fz01or  10067  cbvsum  11323  fsum3  11350  cbvprod  11521  fprodseq  11546  gcdsupex  11912  gcdsupcl  11913  pythagtriplem2  12220  pythagtrip  12237