Theorem orbi2i 255

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

Hypothesis

Ref	Expression
orbi2i.1	|- (ph <-> ps)

Assertion

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

Proof of Theorem orbi2i

Step	Hyp	Ref	Expression
1		orbi2i.1	. . 3 |- (ph <-> ps)
2	1	imbi2i 185	. 2 |- ((-. ch -> ph) <-> (-. ch -> ps))
3		df-or 224	. 2 |- ((ch \/ ph) <-> (-. ch -> ph))
4		df-or 224	. 2 |- ((ch \/ ps) <-> (-. ch -> ps))
5	2, 3, 4	3bitr4 183	1 |- ((ch \/ ph) <-> (ch \/ ps))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222

This theorem is referenced by:  orbi1i 256  orbi12i 257  orass 260  or23 263  or4 264  or42 265  orordir 267  pm4.52 307  pm2.85 581  andi 606  orbidi 745  19.30 1087  19.44 1091  sspsstri 2151  unass 2190  undi 2255  undif4 2329  iinun2 2614  iinuni 2620  iununi 2621  ordtri3or 2985  ordtri2 2988  on0eqelt 3130  fopabap 3847  dfrdg2 3939  psslinpr 5147  suplem2pr 5174  elxr 5547  xrinfmss 6081  elnn0 6103  crrecz 6742  infxpidmlem2 7554  atoml 10304  atoml2 10305

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

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain