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  1535  norass  1538  cadan  1610  19.45v  2000  19.45  2245  3r19.43  3105  unass  4124  tz7.48lem  8372  dffin7-2  10308  zorng  10414  entri2  10468  grothprim  10745  leloe  11219  arch  12398  elznn0nn  12502  xrleloe  13058  swrdnnn0nd  14580  ressval3d  17173  opsrtoslem1  22010  fctop2  22949  alexsubALTlem3  23993  noextenddif  27636  lesloe  27722  precsexlem11  28213  eln0s  28357  bdayfinbndlem1  28463  colinearalg  28983  numclwwlk3lem2  30459  disjnf  32645  ballotlemfc0  34650  ballotlemfcc  34651  satfvsucsuc  35559  satfbrsuc  35560  fmlasuc  35580  ordcmp  36641  wl-df2-3mintru2  37690  poimirlem21  37842  ovoliunnfl  37863  biimpor  38285  tsim1  38331  leatb  39552  expdioph  43265  dflim5  43571  ifpim123g  43741  ifpimimb  43745  ifpororb  43746  rp-fakeinunass  43756  andi3or  44265  uneqsn  44266  sbc3or  44773  en3lpVD  45085  el1fzopredsuc  47571  iccpartgt  47673  fmtno4prmfac  47818  dfvopnbgr2  48099  isubgr3stgrlem4  48215  gpgprismgr4cycllem7  48347  ldepspr  48719