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  3715  uneq1  4160  r19.45zv  4502  rexprgf  4694  rextpg  4698  swopolem  5601  ordsseleq  6412  ordtri3  6419  frxp2  8170  xpord2pred  8171  xpord2indlem  8173  frxp3  8177  xpord3pred  8178  infltoreq  9543  cantnflem1  9730  axgroth2  10866  axgroth3  10872  lelttric  11369  ltxr  13158  xmulneg1  13312  fzpr  13620  elfzp12  13644  caubnd  15398  lcmval  16630  lcmass  16652  isprm6  16752  vdwlem10  17029  irredmul  20430  lringuplu  20545  domneq0  20709  znfld  21580  opsrval  22065  logreclem  26806  perfectlem2  27275  legov3  28607  lnhl  28624  colperpex  28742  lmif  28794  islmib  28796  friendshipgt3  30418  h1datom  31602  xrlelttric  32757  tlt3  32961  prmidl  33469  ismxidl  33491  rprmdvds  33548  esumpcvgval  34080  sibfof  34343  satfvsuc  35367  satfv1  35369  satfvsucsuc  35371  satf0suc  35382  sat1el2xp  35385  fmlasuc0  35390  fmlafvel  35391  satfv1fvfmla1  35429  segcon2  36107  wl-ifpimpr  37468  poimirlem25  37653  cnambfre  37676  pridl  38045  ismaxidl  38048  ispridlc  38078  pridlc  38079  dmnnzd  38083  disjecxrncnvep  38392  4atlem3a  39600  pmapjoin  39855  lcfl3  41497  lcfl4N  41498  sticksstones22  42170  ordsssucb  43353  sbcoreleleqVD  44884  fourierdlem80  46206  euoreqb  47126  el1fzopredsuc  47342  perfectALTVlem2  47714  nnsum3primesle9  47786  clnbupgrel  47826  dfvopnbgr2  47844  lindslinindsimp2  48385