Theorem orbi1d 914

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

Syntax hints:   → wi 4   ↔ wb 209   ∨ wo 844

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 210  df-or 845

This theorem is referenced by:  orbi1  915  orbi12d  916  eueq2  3624  uneq1  4061  r19.45zv  4396  rexprgf  4588  rextpg  4592  swopolem  5452  ordsseleq  6198  ordtri3  6205  infltoreq  8999  cantnflem1  9185  axgroth2  10285  axgroth3  10291  lelttric  10785  ltxr  12551  xmulneg1  12703  fzpr  13011  elfzp12  13035  caubnd  14766  lcmval  15988  lcmass  16010  isprm6  16110  vdwlem10  16381  irredmul  19530  domneq0  20138  znfld  20328  opsrval  20806  logreclem  25447  perfectlem2  25913  legov3  26491  lnhl  26508  colperpex  26626  lmif  26678  islmib  26680  friendshipgt3  28282  h1datom  29464  xrlelttric  30599  tlt3  30774  prmidl  31136  ismxidl  31155  esumpcvgval  31565  sibfof  31826  satfvsuc  32839  satfv1  32841  satfvsucsuc  32843  satf0suc  32854  sat1el2xp  32857  fmlasuc0  32862  fmlafvel  32863  satfv1fvfmla1  32901  frxp2  33346  xpord2pred  33347  xpord2ind  33349  frxp3  33352  xpord3pred  33353  segcon2  33956  wl-ifpimpr  35163  poimirlem25  35362  cnambfre  35385  pridl  35755  ismaxidl  35758  ispridlc  35788  pridlc  35789  dmnnzd  35793  4atlem3a  37173  pmapjoin  37428  lcfl3  39070  lcfl4N  39071  sbcoreleleqVD  41938  fourierdlem80  43194  euoreqb  44033  el1fzopredsuc  44250  perfectALTVlem2  44607  nnsum3primesle9  44679  lindslinindsimp2  45237