Theorem orbi1d 915

Description: Deduction adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 21-Jun-1993.)

Hypothesis

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

Assertion

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

Proof of Theorem orbi1d

Step	Hyp	Ref	Expression
1		bid.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
2	1	orbi2d 914	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
3		orcom 868	. 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓))
4		orcom 868	. 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒))
5	2, 3, 4	3bitr4g 313	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 845

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-or 846

This theorem is referenced by:  orbi1  916  orbi12d  917  eueq2  3697  uneq1  4147  r19.45zv  4491  rexprgf  4685  rextpg  4691  swopolem  5586  ordsseleq  6377  ordtri3  6384  frxp2  8107  xpord2pred  8108  xpord2indlem  8110  frxp3  8114  xpord3pred  8115  infltoreq  9474  cantnflem1  9661  axgroth2  10797  axgroth3  10803  lelttric  11298  ltxr  13072  xmulneg1  13225  fzpr  13533  elfzp12  13557  caubnd  15282  lcmval  16506  lcmass  16528  isprm6  16628  vdwlem10  16900  irredmul  20188  lringuplu  20259  domneq0  20842  znfld  21042  opsrval  21522  logreclem  26187  perfectlem2  26653  legov3  27660  lnhl  27677  colperpex  27795  lmif  27847  islmib  27849  friendshipgt3  29462  h1datom  30644  xrlelttric  31782  tlt3  31957  prmidl  32352  ismxidl  32372  esumpcvgval  32842  sibfof  33105  satfvsuc  34118  satfv1  34120  satfvsucsuc  34122  satf0suc  34133  sat1el2xp  34136  fmlasuc0  34141  fmlafvel  34142  satfv1fvfmla1  34180  segcon2  34842  wl-ifpimpr  36086  poimirlem25  36252  cnambfre  36275  pridl  36645  ismaxidl  36648  ispridlc  36678  pridlc  36679  dmnnzd  36683  disjecxrncnvep  37000  4atlem3a  38208  pmapjoin  38463  lcfl3  40105  lcfl4N  40106  sticksstones22  40724  ordsssucb  41793  sbcoreleleqVD  43328  fourierdlem80  44612  euoreqb  45526  el1fzopredsuc  45742  perfectALTVlem2  46099  nnsum3primesle9  46171  lindslinindsimp2  46729