Theorem orbi1d 930

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

This proof depends on syntax axioms:   → wi 4   ↔ wb 209   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  orbi1  931  orbi12d  932  eueq2  3668  uneq1  4108  r19.45zv  4464  rexprgf  4656  rextpg  4660  swopolem  5569  ordsseleq  6391  ordtri3  6398  frxp2  8154  xpord2pred  8155  xpord2indlem  8157  frxp3  8161  xpord3pred  8162  infltoreq  9489  cantnflem1  9683  axgroth2  10903  axgroth3  10909  lelttric  11410  ltxr  13237  xmulneg1  13392  fzpr  13706  elfzp12  13730  caubnd  15519  lcmval  16760  lcmass  16782  isprm6  16883  vdwlem10  17161  irredmul  20652  lringuplu  20789  domneq0  20953  prmidl  21614  prmidlprop  21625  znfld  21859  opsrval  22348  logreclem  27083  perfectlem2  27550  nnm1n0s  28754  bdaypw2n0bndlem  28842  legov3  29054  lnhl  29074  colperpex  29202  lmif  29283  islmib  29285  friendshipgt3  30992  h1datom  32177  xrlelttric  33337  tlt3  33524  domnprodeq0  33833  ismxidl  33980  rprmdvds  34044  esumpcvgval  34703  sibfof  34965  satfvsuc  36105  satfv1  36107  satfvsucsuc  36109  satf0suc  36120  sat1el2xp  36123  fmlasuc0  36128  fmlafvel  36129  satfv1fvfmla1  36167  segcon2  36850  axtcond  37246  wl-ifpimpr  38369  poimirlem25  38543  cnambfre  38566  varprop  38622  negprop  38623  impprop  38624  dfprop2  38626  pridl  38951  ismaxidl  38954  ispridlc  38984  pridlc  38985  dmnnzd  38989  disjecxrncnvep  39325  4atlem3a  40634  pmapjoin  40889  lcfl3  42531  lcfl4N  42532  sticksstones22  43198  quadfac  43235  ordsssucb  44321  sbcoreleleqVD  45826  fourierdlem80  47165  euoreqb  48148  el1fzopredsuc  48365  perfectALTVlem2  48789  nnsum3primesle9  48861  clnbupgrel  48901  dfvopnbgr2  48920  idomnzd  49412  lindslinindsimp2  49544