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  5542  ordsseleq  6346  ordtri3  6353  frxp2  8087  xpord2pred  8088  xpord2indlem  8090  frxp3  8094  xpord3pred  8095  infltoreq  9410  cantnflem1  9601  axgroth2  10739  axgroth3  10745  lelttric  11244  ltxr  13057  xmulneg1  13212  fzpr  13524  elfzp12  13548  caubnd  15312  lcmval  16552  lcmass  16574  isprm6  16675  vdwlem10  16952  irredmul  20400  lringuplu  20512  domneq0  20676  znfld  21550  opsrval  22034  logreclem  26739  perfectlem2  27207  nnm1n0s  28381  bdaypw2n0bndlem  28469  legov3  28680  lnhl  28697  colperpex  28815  lmif  28867  islmib  28869  friendshipgt3  30483  h1datom  31668  xrlelttric  32840  tlt3  33045  domnprodeq0  33352  prmidl  33515  ismxidl  33537  rprmdvds  33594  esumpcvgval  34238  sibfof  34500  satfvsuc  35559  satfv1  35561  satfvsucsuc  35563  satf0suc  35574  sat1el2xp  35577  fmlasuc0  35582  fmlafvel  35583  satfv1fvfmla1  35621  segcon2  36303  axtcond  36676  wl-ifpimpr  37796  poimirlem25  37980  cnambfre  38003  pridl  38372  ismaxidl  38375  ispridlc  38405  pridlc  38406  dmnnzd  38410  disjecxrncnvep  38748  4atlem3a  40057  pmapjoin  40312  lcfl3  41954  lcfl4N  41955  sticksstones22  42621  ordsssucb  43781  sbcoreleleqVD  45303  fourierdlem80  46632  euoreqb  47569  el1fzopredsuc  47786  perfectALTVlem2  48210  nnsum3primesle9  48282  clnbupgrel  48322  dfvopnbgr2  48341  lindslinindsimp2  48951