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 285	1 ⊢ ((𝜑 ∨ 𝜒) ↔ (𝜓 ∨ 𝜒))

Syntax hints:   ↔ 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:  orbi12i  542  orordi  551  3anor  1047  3or6  1402  cadan  1539  19.45v  1900  19.45  2094  unass  3732  tz7.48lem  7423  dffin7-2  9103  zorng  9209  entri2  9259  grothprim  9535  leloe  10003  arch  11166  elznn0nn  11268  xrleloe  11853  ressval3d  15764  opsrtoslem1  19305  fctop2  20619  alexsubALTlem3  21663  colinearalg  25590  cusgrasizeindslem1  26002  disjnf  28766  ballotlemfc0  29881  ballotlemfcc  29882  ordcmp  31616  bj-nfn  31795  poimirlem21  32600  ovoliunnfl  32621  biimpor  33053  tsim1  33107  leatb  33597  expdioph  36608  ifpim123g  36864  ifpimimb  36868  ifpororb  36869  rp-fakeinunass  36880  andi3or  37340  uneqsn  37341  sbc3or  37759  en3lpVD  38102  el1fzopredsuc  39948  iccpartgt  39965  fmtno4prmfac  40022  ldepspr  42056