Theorem orbi1d 915

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

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

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 847

This theorem is referenced by:  orbi1  916  orbi12d  917  eueq2  3732  uneq1  4184  r19.45zv  4526  rexprgf  4718  rextpg  4724  swopolem  5618  ordsseleq  6424  ordtri3  6431  frxp2  8185  xpord2pred  8186  xpord2indlem  8188  frxp3  8192  xpord3pred  8193  infltoreq  9571  cantnflem1  9758  axgroth2  10894  axgroth3  10900  lelttric  11397  ltxr  13178  xmulneg1  13331  fzpr  13639  elfzp12  13663  caubnd  15407  lcmval  16639  lcmass  16661  isprm6  16761  vdwlem10  17037  irredmul  20455  lringuplu  20570  domneq0  20730  znfld  21602  opsrval  22087  logreclem  26823  perfectlem2  27292  legov3  28624  lnhl  28641  colperpex  28759  lmif  28811  islmib  28813  friendshipgt3  30430  h1datom  31614  xrlelttric  32759  tlt3  32943  prmidl  33433  ismxidl  33455  rprmdvds  33512  esumpcvgval  34042  sibfof  34305  satfvsuc  35329  satfv1  35331  satfvsucsuc  35333  satf0suc  35344  sat1el2xp  35347  fmlasuc0  35352  fmlafvel  35353  satfv1fvfmla1  35391  segcon2  36069  wl-ifpimpr  37432  poimirlem25  37605  cnambfre  37628  pridl  37997  ismaxidl  38000  ispridlc  38030  pridlc  38031  dmnnzd  38035  disjecxrncnvep  38346  4atlem3a  39554  pmapjoin  39809  lcfl3  41451  lcfl4N  41452  sticksstones22  42125  ordsssucb  43297  sbcoreleleqVD  44830  fourierdlem80  46107  euoreqb  47024  el1fzopredsuc  47240  perfectALTVlem2  47596  nnsum3primesle9  47668  clnbupgrel  47707  dfvopnbgr2  47725  lindslinindsimp2  48192