Theorem orbi1d 913

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

Syntax hints:   → wi 4   ↔ wb 205   ∨ wo 843

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 206  df-or 844

This theorem is referenced by:  orbi1  914  orbi12d  915  eueq2  3640  uneq1  4086  r19.45zv  4430  rexprgf  4626  rextpg  4632  swopolem  5504  ordsseleq  6280  ordtri3  6287  infltoreq  9191  cantnflem1  9377  axgroth2  10512  axgroth3  10518  lelttric  11012  ltxr  12780  xmulneg1  12932  fzpr  13240  elfzp12  13264  caubnd  14998  lcmval  16225  lcmass  16247  isprm6  16347  vdwlem10  16619  irredmul  19866  domneq0  20481  znfld  20680  opsrval  21157  logreclem  25817  perfectlem2  26283  legov3  26863  lnhl  26880  colperpex  26998  lmif  27050  islmib  27052  friendshipgt3  28663  h1datom  29845  xrlelttric  30977  tlt3  31150  prmidl  31517  ismxidl  31536  esumpcvgval  31946  sibfof  32207  satfvsuc  33223  satfv1  33225  satfvsucsuc  33227  satf0suc  33238  sat1el2xp  33241  fmlasuc0  33246  fmlafvel  33247  satfv1fvfmla1  33285  frxp2  33718  xpord2pred  33719  xpord2ind  33721  frxp3  33724  xpord3pred  33725  segcon2  34334  wl-ifpimpr  35564  poimirlem25  35729  cnambfre  35752  pridl  36122  ismaxidl  36125  ispridlc  36155  pridlc  36156  dmnnzd  36160  4atlem3a  37538  pmapjoin  37793  lcfl3  39435  lcfl4N  39436  sticksstones22  40052  sbcoreleleqVD  42368  fourierdlem80  43617  euoreqb  44488  el1fzopredsuc  44705  perfectALTVlem2  45062  nnsum3primesle9  45134  lindslinindsimp2  45692