Theorem orbi1d 922

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

Syntax hints:   → wi 4   ↔ wb 207   ∨ wo 853

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 208  df-or 854

This theorem is referenced by:  orbi1  923  orbi12d  924  eueq2  3651  uneq1  4091  r19.45zv  4436  rexprgf  4627  rextpg  4631  swopolem  5536  ordsseleq  6339  ordtri3  6346  frxp2  8084  xpord2pred  8085  xpord2indlem  8087  frxp3  8091  xpord3pred  8092  infltoreq  9407  cantnflem1  9601  axgroth2  10739  axgroth3  10745  lelttric  11244  ltxr  13057  xmulneg1  13212  fzpr  13524  elfzp12  13548  caubnd  15312  lcmval  16552  lcmass  16574  isprm6  16675  vdwlem10  16952  irredmul  20400  lringuplu  20516  domneq0  20680  znfld  21535  opsrval  22022  logreclem  26744  perfectlem2  27211  nnm1n0s  28385  bdaypw2n0bndlem  28473  legov3  28684  lnhl  28701  colperpex  28819  lmif  28871  islmib  28873  friendshipgt3  30486  h1datom  31671  xrlelttric  32844  tlt3  33049  domnprodeq0  33357  prmidl  33523  ismxidl  33545  rprmdvds  33602  esumpcvgval  34262  sibfof  34524  satfvsuc  35589  satfv1  35591  satfvsucsuc  35593  satf0suc  35604  sat1el2xp  35607  fmlasuc0  35612  fmlafvel  35613  satfv1fvfmla1  35651  segcon2  36333  axtcond  36706  wl-ifpimpr  37828  poimirlem25  38012  cnambfre  38035  pridl  38404  ismaxidl  38407  ispridlc  38437  pridlc  38438  dmnnzd  38442  disjecxrncnvep  38780  4atlem3a  40089  pmapjoin  40344  lcfl3  41986  lcfl4N  41987  sticksstones22  42653  ordsssucb  43780  sbcoreleleqVD  45302  fourierdlem80  46629  euoreqb  47572  el1fzopredsuc  47789  perfectALTVlem2  48213  nnsum3primesle9  48285  clnbupgrel  48325  dfvopnbgr2  48344  lindslinindsimp2  48954