Theorem orbi1d 917

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

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

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 849

This theorem is referenced by:  orbi1  918  orbi12d  919  eueq2  3657  uneq1  4102  r19.45zv  4449  rexprgf  4640  rextpg  4644  swopolem  5540  ordsseleq  6344  ordtri3  6351  frxp2  8085  xpord2pred  8086  xpord2indlem  8088  frxp3  8092  xpord3pred  8093  infltoreq  9408  cantnflem1  9599  axgroth2  10737  axgroth3  10743  lelttric  11242  ltxr  13055  xmulneg1  13210  fzpr  13522  elfzp12  13546  caubnd  15310  lcmval  16550  lcmass  16572  isprm6  16673  vdwlem10  16950  irredmul  20398  lringuplu  20510  domneq0  20674  znfld  21548  opsrval  22033  logreclem  26743  perfectlem2  27212  nnm1n0s  28386  bdaypw2n0bndlem  28474  legov3  28685  lnhl  28702  colperpex  28820  lmif  28872  islmib  28874  friendshipgt3  30488  h1datom  31673  xrlelttric  32845  tlt3  33050  domnprodeq0  33357  prmidl  33520  ismxidl  33542  rprmdvds  33599  esumpcvgval  34243  sibfof  34505  satfvsuc  35564  satfv1  35566  satfvsucsuc  35568  satf0suc  35579  sat1el2xp  35582  fmlasuc0  35587  fmlafvel  35588  satfv1fvfmla1  35626  segcon2  36308  axtcond  36681  wl-ifpimpr  37793  poimirlem25  37977  cnambfre  38000  pridl  38369  ismaxidl  38372  ispridlc  38402  pridlc  38403  dmnnzd  38407  disjecxrncnvep  38745  4atlem3a  40054  pmapjoin  40309  lcfl3  41951  lcfl4N  41952  sticksstones22  42618  ordsssucb  43778  sbcoreleleqVD  45300  fourierdlem80  46629  euoreqb  47554  el1fzopredsuc  47771  perfectALTVlem2  48195  nnsum3primesle9  48267  clnbupgrel  48307  dfvopnbgr2  48326  lindslinindsimp2  48936