Theorem orbi1d 734

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

Syntax hints:   → wi 4   ↔ wb 194   ∨ wo 381

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 195  df-or 383

This theorem is referenced by:  orbi1  737  orbi12d  741  eueq2  3346  uneq1  3721  r19.45zv  4019  rexprg  4181  rextpg  4183  swopolem  4958  ordsseleq  5655  ordtri3  5662  infltoreq  8268  cantnflem1  8446  axgroth2  9503  axgroth3  9509  lelttric  9995  ltxr  11784  xmulneg1  11928  fzpr  12221  elfzp12  12243  caubnd  13892  lcmval  15089  lcmass  15111  isprm6  15210  vdwlem10  15478  irredmul  18478  domneq0  19064  opsrval  19241  znfld  19673  logreclem  24217  perfectlem2  24672  legov3  25211  lnhl  25228  colperpex  25343  lmif  25395  islmib  25397  friendshipgt3  26414  h1datom  27631  xrlelttric  28712  tlt3  28802  esumpcvgval  29273  sibfof  29535  nofulllem5  30911  segcon2  31188  poimirlem25  32400  cnambfre  32424  pridl  32802  ismaxidl  32805  ispridlc  32835  pridlc  32836  dmnnzd  32840  4atlem3a  33697  pmapjoin  33952  lcfl3  35597  lcfl4N  35598  sbc3orgOLD  37559  fourierdlem80  38876  el1fzopredsuc  39746  perfectALTVlem2  39963  nnsum3primesle9  40008  av-friendshipgt3  41547  lindslinindsimp2  42041