Theorem orbi1i 542

Description: Inference adding a right disjunct to both sides of a logical equivalence. (Contributed by NM, 3-Jan-1993.)

Hypothesis

Ref	Expression
orbi2i.1	⊢ (𝜑 ↔ 𝜓)

Assertion

Ref	Expression
orbi1i	⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Proof of Theorem orbi1i

Step	Hyp	Ref	Expression
1		orcom 402	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 541	. 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
4		orcom 402	. 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
5	1, 3, 4	3bitri 286	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Syntax hints:   ↔ wb 196   ∨ wo 383

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 385

This theorem is referenced by:  orbi12i  543  orordi  552  3anor  1054  3or6  1410  cadan  1548  nfnbi  1781  19.45v  1913  19.45  2107  unass  3770  tz7.48lem  7536  dffin7-2  9220  zorng  9326  entri2  9380  grothprim  9656  leloe  10124  arch  11289  elznn0nn  11391  xrleloe  11977  ressval3d  15937  opsrtoslem1  19484  fctop2  20809  alexsubALTlem3  21853  colinearalg  25790  disjnf  29384  ballotlemfc0  30554  ballotlemfcc  30555  noextenddif  31821  sleloe  31879  ordcmp  32446  poimirlem21  33430  ovoliunnfl  33451  biimpor  33883  tsim1  33937  leatb  34579  expdioph  37590  ifpim123g  37845  ifpimimb  37849  ifpororb  37850  rp-fakeinunass  37861  andi3or  38320  uneqsn  38321  sbc3or  38738  en3lpVD  39080  el1fzopredsuc  41335  iccpartgt  41363  fmtno4prmfac  41484  ldepspr  42262