Theorem orbi2d 797

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 144	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3	2	orim2d 795	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) → (𝜃 ∨ 𝜒)))
4	1	biimprd 158	. . 3 ⊢ (𝜑 → (𝜒 → 𝜓))
5	4	orim2d 795	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜒) → (𝜃 ∨ 𝜓)))
6	3, 5	impbid 129	1 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))

Syntax hints:   → wi 4   ↔ wb 105   ∨ wo 715

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

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  798  orbi12d  800  dn1dc  968  xorbi2d  1424  eueq2dc  2979  r19.44mv  3589  rexprg  3721  rextpg  3723  exmidsssn  4292  exmidsssnc  4293  swopolem  4402  sowlin  4417  elsucg  4501  elsuc2g  4502  ordsoexmid  4660  poleloe  5136  funopsn  5830  isosolem  5965  freceq2  6559  brdifun  6729  pitric  7541  elinp  7694  prloc  7711  ltexprlemloc  7827  suplocexprlemloc  7941  ltsosr  7984  aptisr  7999  suplocsrlemb  8026  axpre-ltwlin  8103  axpre-suploclemres  8121  axpre-suploc  8122  gt0add  8753  apreap  8767  apreim  8783  elznn0  9494  elznn  9495  peano2z  9515  zindd  9598  elfzp1  10307  fzm1  10335  fzosplitsni  10482  cjap  11471  dvdslelemd  12409  zeo5  12454  lcmval  12640  lcmneg  12651  lcmass  12662  isprm6  12724  infpn2  13082  gsumsplit0  13938  lringuplu  14216  domneq0  14292  znidom  14677  dedekindeulemloc  15349  dedekindeulemeu  15352  suplociccreex  15354  dedekindicclemloc  15358  dedekindicclemeu  15361  bj-charfunr  16431  bj-nn0sucALT  16599