Theorem orbi2d 790

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1d  791  orbi12d  793  dn1dc  960  xorbi2d  1380  eueq2dc  2910  r19.44mv  3517  rexprg  3644  rextpg  3646  exmidsssn  4202  exmidsssnc  4203  swopolem  4305  sowlin  4320  elsucg  4404  elsuc2g  4405  ordsoexmid  4561  poleloe  5028  isosolem  5824  freceq2  6393  brdifun  6561  pitric  7319  elinp  7472  prloc  7489  ltexprlemloc  7605  suplocexprlemloc  7719  ltsosr  7762  aptisr  7777  suplocsrlemb  7804  axpre-ltwlin  7881  axpre-suploclemres  7899  axpre-suploc  7900  gt0add  8529  apreap  8543  apreim  8559  elznn0  9267  elznn  9268  peano2z  9288  zindd  9370  elfzp1  10071  fzm1  10099  fzosplitsni  10234  cjap  10914  dvdslelemd  11848  zeo5  11892  lcmval  12062  lcmneg  12073  lcmass  12084  isprm6  12146  infpn2  12456  lringuplu  13335  dedekindeulemloc  14067  dedekindeulemeu  14070  suplociccreex  14072  dedekindicclemloc  14076  dedekindicclemeu  14079  bj-charfunr  14532  bj-nn0sucALT  14700