Theorem orbi1d 916

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

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

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 848

This theorem is referenced by:  orbi1  917  orbi12d  918  eueq2  3678  uneq1  4120  r19.45zv  4462  rexprgf  4655  rextpg  4659  swopolem  5549  ordsseleq  6349  ordtri3  6356  frxp2  8100  xpord2pred  8101  xpord2indlem  8103  frxp3  8107  xpord3pred  8108  infltoreq  9431  cantnflem1  9618  axgroth2  10754  axgroth3  10760  lelttric  11257  ltxr  13051  xmulneg1  13205  fzpr  13516  elfzp12  13540  caubnd  15301  lcmval  16538  lcmass  16560  isprm6  16660  vdwlem10  16937  irredmul  20314  lringuplu  20429  domneq0  20593  znfld  21446  opsrval  21929  logreclem  26648  perfectlem2  27117  nnm1n0s  28240  legov3  28501  lnhl  28518  colperpex  28636  lmif  28688  islmib  28690  friendshipgt3  30300  h1datom  31484  xrlelttric  32648  tlt3  32869  prmidl  33384  ismxidl  33406  rprmdvds  33463  esumpcvgval  34041  sibfof  34304  satfvsuc  35321  satfv1  35323  satfvsucsuc  35325  satf0suc  35336  sat1el2xp  35339  fmlasuc0  35344  fmlafvel  35345  satfv1fvfmla1  35383  segcon2  36066  wl-ifpimpr  37427  poimirlem25  37612  cnambfre  37635  pridl  38004  ismaxidl  38007  ispridlc  38037  pridlc  38038  dmnnzd  38042  disjecxrncnvep  38349  4atlem3a  39564  pmapjoin  39819  lcfl3  41461  lcfl4N  41462  sticksstones22  42129  ordsssucb  43297  sbcoreleleqVD  44821  fourierdlem80  46157  euoreqb  47083  el1fzopredsuc  47299  perfectALTVlem2  47696  nnsum3primesle9  47768  clnbupgrel  47808  dfvopnbgr2  47826  lindslinindsimp2  48425