Theorem orbi2d 737

Description: Deduction adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Revised by Mario Carneiro, 31-Jan-2015.)

Hypothesis

Ref	Expression
orbid.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
orbi2d	⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Proof of Theorem orbi2d

Step	Hyp	Ref	Expression
1		orbid.1	. . . 4 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	biimpd 142	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	orim2d 735	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
4	1	biimprd 156	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
5	4	orim2d 735	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓)))
6	3, 5	impbid 127	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 103   ∨ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  orbi1d  738  orbi12d  740  dn1dc  902  xorbi2d  1312  eueq2dc  2774  r19.44mv  3352  rexprg  3462  rextpg  3464  swopolem  4088  sowlin  4103  elsucg  4187  elsuc2g  4188  ordsoexmid  4333  poleloe  4774  isosolem  5515  freceq2  6063  brdifun  6221  pitric  6643  elinp  6796  prloc  6813  ltexprlemloc  6929  ltsosr  7073  aptisr  7087  axpre-ltwlin  7181  gt0add  7810  apreap  7824  apreim  7840  elznn0  8517  elznn  8518  peano2z  8538  zindd  8616  elfzp1  9235  fzm1  9263  fzosplitsni  9391  cjap  10012  dvdslelemd  10469  zeo5  10513  lcmval  10670  lcmneg  10681  lcmass  10692  isprm6  10751  bj-nn0sucALT  11058