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 577  andi 602  orbidi 741  19.30 1081  19.44 1085  sspsstri 2138  unass 2177  undi 2242  undif4 2315  iinun2 2599  iinuni 2605  iununi 2606  ordtri3or 2969  ordtri2 2972  on0eqelt 3114  fopabap 3826  dfrdg2 3918  psslinpr 5107  suplem2pr 5134  elxr 5508  xrinfmss 6026  elnn0 6048  crrecz 6672  infxpidmlem2 7496  atoml 10217  atoml2 10218

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