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  5573  ordsseleq  6387  ordtri3  6394  frxp2  8142  xpord2pred  8143  xpord2indlem  8145  frxp3  8149  xpord3pred  8150  infltoreq  9474  cantnflem1  9668  axgroth2  10834  axgroth3  10840  lelttric  11341  ltxr  13166  xmulneg1  13321  fzpr  13634  elfzp12  13658  caubnd  15446  lcmval  16682  lcmass  16704  isprm6  16805  vdwlem10  17082  irredmul  20570  lringuplu  20706  domneq0  20870  prmidl  21528  prmidlprop  21539  znfld  21773  opsrval  22262  logreclem  26999  perfectlem2  27466  nnm1n0s  28640  bdaypw2n0bndlem  28728  legov3  28940  lnhl  28960  colperpex  29088  lmif  29169  islmib  29171  friendshipgt3  30878  h1datom  32063  xrlelttric  33223  tlt3  33410  domnprodeq0  33719  ismxidl  33865  rprmdvds  33929  esumpcvgval  34588  sibfof  34851  satfvsuc  35940  satfv1  35942  satfvsucsuc  35944  satf0suc  35955  sat1el2xp  35958  fmlasuc0  35963  fmlafvel  35964  satfv1fvfmla1  36002  segcon2  36685  axtcond  37097  wl-ifpimpr  38220  poimirlem25  38394  cnambfre  38417  pridl  38787  ismaxidl  38790  ispridlc  38820  pridlc  38821  dmnnzd  38825  disjecxrncnvep  39161  4atlem3a  40470  pmapjoin  40725  lcfl3  42367  lcfl4N  42368  sticksstones22  43034  quadfac  43071  ordsssucb  44176  sbcoreleleqVD  45681  fourierdlem80  47014  euoreqb  47997  el1fzopredsuc  48214  perfectALTVlem2  48638  nnsum3primesle9  48710  clnbupgrel  48750  dfvopnbgr2  48769  idomnzd  49261  lindslinindsimp2  49393