Theorem orbi1d 735

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

Syntax hints:   → wi 4   ↔ wb 195   ∨ 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 196  df-or 384

This theorem is referenced by:  orbi1  738  orbi12d  742  eueq2  3347  uneq1  3722  r19.45zv  4020  rexprg  4182  rextpg  4184  swopolem  4968  ordsseleq  5669  ordtri3  5676  infltoreq  8291  cantnflem1  8469  axgroth2  9526  axgroth3  9532  lelttric  10023  ltxr  11825  xmulneg1  11971  fzpr  12266  elfzp12  12288  caubnd  13946  lcmval  15143  lcmass  15165  isprm6  15264  vdwlem10  15532  irredmul  18532  domneq0  19118  opsrval  19295  znfld  19728  logreclem  24300  perfectlem2  24755  legov3  25293  lnhl  25310  colperpex  25425  lmif  25477  islmib  25479  friendshipgt3  26648  h1datom  27825  xrlelttric  28906  tlt3  28996  esumpcvgval  29467  sibfof  29729  nofulllem5  31105  segcon2  31382  poimirlem25  32604  cnambfre  32628  pridl  33006  ismaxidl  33009  ispridlc  33039  pridlc  33040  dmnnzd  33044  4atlem3a  33901  pmapjoin  34156  lcfl3  35801  lcfl4N  35802  sbc3orgOLD  37763  fourierdlem80  39079  el1fzopredsuc  39948  perfectALTVlem2  40165  nnsum3primesle9  40210  av-friendshipgt3  41552  lindslinindsimp2  42046