Theorem orbi2i 214

Description: Inference adding a left disjunct to both sides of a logical equivalence.

Hypothesis

Ref	Expression
bi.oa	|- (ph <-> ps)

Assertion

Ref	Expression
orbi2i	|- ((ch \/ ph) <-> (ch \/ ps))

Proof of Theorem orbi2i

Step	Hyp	Ref	Expression
1		bi.oa	. . 3 |- (ph <-> ps)
2	1	imbi2i 160	. 2 |- ((-. ch -> ph) <-> (-. ch -> ps))
3		df-or 197	. 2 |- ((ch \/ ph) <-> (-. ch -> ph))
4		df-or 197	. 2 |- ((ch \/ ps) <-> (-. ch -> ps))
5	2, 3, 4	3bitr4 158	1 |- ((ch \/ ph) <-> (ch \/ ps))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195

This theorem is referenced by:  orbi1i 215  orbi12i 216  orass 218  or23 219  or4 220  or42 221  orordir 223  pm2.85 439  andi 456  orbidi 510  biass 511  19.30 764  19.44 768  sbc2or 1454  sspsstri 1572  unass 1615  undi 1677  undif4 1744  iinun2 2031  iinuni 2036  iununi 2037  ordtri3or 2230  ordtri2 2233  on0eqelt 2370  psslinpr 3929  suplem2pr 3956  elnn0 4536  infxpidmlem2 4934

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org