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

Syntax hints:   → wi 4   ↔ wb 205   ∨ 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 206  df-or 845

This theorem is referenced by:  orbi1  914  orbi12d  915  eueq2  3698  uneq1  4148  r19.45zv  4494  rexprgf  4689  rextpg  4695  swopolem  5588  ordsseleq  6383  ordtri3  6390  frxp2  8124  xpord2pred  8125  xpord2indlem  8127  frxp3  8131  xpord3pred  8132  infltoreq  9493  cantnflem1  9680  axgroth2  10816  axgroth3  10822  lelttric  11318  ltxr  13092  xmulneg1  13245  fzpr  13553  elfzp12  13577  caubnd  15302  lcmval  16526  lcmass  16548  isprm6  16648  vdwlem10  16922  irredmul  20321  lringuplu  20434  domneq0  21197  znfld  21423  opsrval  21911  logreclem  26610  perfectlem2  27079  legov3  28318  lnhl  28335  colperpex  28453  lmif  28505  islmib  28507  friendshipgt3  30120  h1datom  31304  xrlelttric  32434  tlt3  32607  prmidl  33027  ismxidl  33047  esumpcvgval  33565  sibfof  33828  satfvsuc  34841  satfv1  34843  satfvsucsuc  34845  satf0suc  34856  sat1el2xp  34859  fmlasuc0  34864  fmlafvel  34865  satfv1fvfmla1  34903  segcon2  35572  wl-ifpimpr  36837  poimirlem25  37003  cnambfre  37026  pridl  37395  ismaxidl  37398  ispridlc  37428  pridlc  37429  dmnnzd  37433  disjecxrncnvep  37750  4atlem3a  38958  pmapjoin  39213  lcfl3  40855  lcfl4N  40856  sticksstones22  41477  ordsssucb  42574  sbcoreleleqVD  44109  fourierdlem80  45387  euoreqb  46302  el1fzopredsuc  46518  perfectALTVlem2  46875  nnsum3primesle9  46947  lindslinindsimp2  47332