Theorem orbi1i 541

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 401	. 2 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜒 ∨ 𝜑))
2		orbi2i.1	. . 3 ⊢ (𝜑 ↔ 𝜓)
3	2	orbi2i 540	. 2 ⊢ ((𝜒 ∨ 𝜑) ↔ (𝜒 ∨ 𝜓))
4		orcom 401	. 2 ⊢ ((𝜒 ∨ 𝜓) ↔ (𝜓 ∨ 𝜒))
5	1, 3, 4	3bitri 286	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Syntax hints:   ↔ 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:  orbi12i  542  orordi  551  3anorOLD  1072  3ianor  1074  3or6  1450  cadan  1588  nfnbi  1821  19.45v  1969  19.45  2145  unass  3803  tz7.48lem  7581  dffin7-2  9258  zorng  9364  entri2  9418  grothprim  9694  leloe  10162  arch  11327  elznn0nn  11429  xrleloe  12015  ressval3d  15984  opsrtoslem1  19532  fctop2  20857  alexsubALTlem3  21900  colinearalg  25835  numclwwlk3lem  27371  disjnf  29510  ballotlemfc0  30682  ballotlemfcc  30683  noextenddif  31946  sleloe  32004  ordcmp  32571  poimirlem21  33560  ovoliunnfl  33581  biimpor  34013  tsim1  34067  leatb  34897  expdioph  37907  ifpim123g  38162  ifpimimb  38166  ifpororb  38167  rp-fakeinunass  38178  andi3or  38637  uneqsn  38638  sbc3or  39055  en3lpVD  39394  el1fzopredsuc  41660  iccpartgt  41688  fmtno4prmfac  41809  ldepspr  42587