Theorem orbi1d 739

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

Syntax hints:   → wi 4   ↔ wb 196   ∨ wo 382

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 197  df-or 384

This theorem is referenced by:  orbi1  742  orbi12d  746  eueq2  3413  uneq1  3793  r19.45zv  4101  rexprg  4267  rextpg  4269  swopolem  5073  ordsseleq  5790  ordtri3  5797  infltoreq  8449  cantnflem1  8624  axgroth2  9685  axgroth3  9691  lelttric  10182  ltxr  11987  xmulneg1  12137  fzpr  12434  elfzp12  12457  caubnd  14142  lcmval  15352  lcmass  15374  isprm6  15473  vdwlem10  15741  irredmul  18755  domneq0  19345  opsrval  19522  znfld  19957  logreclem  24545  perfectlem2  25000  legov3  25538  lnhl  25555  colperpex  25670  lmif  25722  islmib  25724  friendshipgt3  27385  h1datom  28569  xrlelttric  29645  tlt3  29793  esumpcvgval  30268  sibfof  30530  segcon2  32337  poimirlem25  33564  cnambfre  33588  pridl  33966  ismaxidl  33969  ispridlc  33999  pridlc  34000  dmnnzd  34004  4atlem3a  35201  pmapjoin  35456  lcfl3  37100  lcfl4N  37101  sbc3orgOLD  39059  fourierdlem80  40721  el1fzopredsuc  41660  perfectALTVlem2  41956  nnsum3primesle9  42007  lindslinindsimp2  42577