Theorem orbi1d 916

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 915	. 2 ⊢ (𝜑 → ((𝜃 ∨ 𝜓) ↔ (𝜃 ∨ 𝜒)))
3		orcom 870	. 2 ⊢ ((𝜓 ∨ 𝜃) ↔ (𝜃 ∨ 𝜓))
4		orcom 870	. 2 ⊢ ((𝜒 ∨ 𝜃) ↔ (𝜃 ∨ 𝜒))
5	2, 3, 4	3bitr4g 314	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) ↔ (𝜒 ∨ 𝜃)))

Syntax hints:   → wi 4   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi1  917  orbi12d  918  eueq2  3681  uneq1  4124  r19.45zv  4466  rexprgf  4659  rextpg  4663  swopolem  5556  ordsseleq  6361  ordtri3  6368  frxp2  8123  xpord2pred  8124  xpord2indlem  8126  frxp3  8130  xpord3pred  8131  infltoreq  9455  cantnflem1  9642  axgroth2  10778  axgroth3  10784  lelttric  11281  ltxr  13075  xmulneg1  13229  fzpr  13540  elfzp12  13564  caubnd  15325  lcmval  16562  lcmass  16584  isprm6  16684  vdwlem10  16961  irredmul  20338  lringuplu  20453  domneq0  20617  znfld  21470  opsrval  21953  logreclem  26672  perfectlem2  27141  nnm1n0s  28264  legov3  28525  lnhl  28542  colperpex  28660  lmif  28712  islmib  28714  friendshipgt3  30327  h1datom  31511  xrlelttric  32675  tlt3  32896  prmidl  33411  ismxidl  33433  rprmdvds  33490  esumpcvgval  34068  sibfof  34331  satfvsuc  35348  satfv1  35350  satfvsucsuc  35352  satf0suc  35363  sat1el2xp  35366  fmlasuc0  35371  fmlafvel  35372  satfv1fvfmla1  35410  segcon2  36093  wl-ifpimpr  37454  poimirlem25  37639  cnambfre  37662  pridl  38031  ismaxidl  38034  ispridlc  38064  pridlc  38065  dmnnzd  38069  disjecxrncnvep  38376  4atlem3a  39591  pmapjoin  39846  lcfl3  41488  lcfl4N  41489  sticksstones22  42156  ordsssucb  43324  sbcoreleleqVD  44848  fourierdlem80  46184  euoreqb  47107  el1fzopredsuc  47323  perfectALTVlem2  47720  nnsum3primesle9  47792  clnbupgrel  47832  dfvopnbgr2  47850  lindslinindsimp2  48449