Theorem orbi1i 913

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

Syntax hints:   ↔ wb 206   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  orbi12i  914  orordi  928  3ianor  1106  3or6  1449  norasslem1  1534  norass  1537  cadan  1609  19.45v  1999  19.45  2239  3r19.43  3102  unass  4131  tz7.48lem  8386  dffin7-2  10327  zorng  10433  entri2  10487  grothprim  10763  leloe  11236  arch  12415  elznn0nn  12519  xrleloe  13080  swrdnnn0nd  14597  ressval3d  17192  opsrtoslem1  21938  fctop2  22868  alexsubALTlem3  23912  noextenddif  27556  sleloe  27642  precsexlem11  28095  eln0s  28227  colinearalg  28813  numclwwlk3lem2  30286  disjnf  32472  ballotlemfc0  34457  ballotlemfcc  34458  satfvsucsuc  35325  satfbrsuc  35326  fmlasuc  35346  ordcmp  36408  wl-df2-3mintru2  37446  poimirlem21  37608  ovoliunnfl  37629  biimpor  38051  tsim1  38097  leatb  39258  expdioph  42985  dflim5  43291  ifpim123g  43462  ifpimimb  43466  ifpororb  43467  rp-fakeinunass  43477  andi3or  43986  uneqsn  43987  sbc3or  44495  en3lpVD  44807  el1fzopredsuc  47299  iccpartgt  47401  fmtno4prmfac  47546  dfvopnbgr2  47826  isubgr3stgrlem4  47941  gpgprismgr4cycllem7  48064  ldepspr  48435