Theorem orbi2d 714

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 136	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	orim2d 712	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
4	1	biimprd 151	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
5	4	orim2d 712	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓)))
6	3, 5	impbid 124	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 102   ∨ wo 639

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

This theorem depends on definitions:  df-bi 114

This theorem is referenced by:  orbi1d  715  orbi12d  717  dn1dc  878  xorbi2d  1287  eueq2dc  2736  rexprg  3449  rextpg  3451  swopolem  4069  sowlin  4084  elsucg  4168  elsuc2g  4169  ordsoexmid  4313  poleloe  4751  isosolem  5490  freceq2  6010  brdifun  6163  pitric  6476  elinp  6629  prloc  6646  ltexprlemloc  6762  ltsosr  6906  aptisr  6920  axpre-ltwlin  7014  gt0add  7637  apreap  7651  apreim  7667  elznn0  8316  elznn  8317  peano2z  8337  zindd  8414  elfzp1  9035  fzm1  9063  fzosplitsni  9192  cjap  9733  dvdslelemd  10154  zeo5  10199  bj-nn0sucALT  10469