Theorem orbi2i 763

Description: Inference adding a left disjunct to both sides of a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 12-Dec-2012.)

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	. . . 4 |- ( ph <-> ps )
2	1	biimpi 120	. . 3 |- ( ph -> ps )
3	2	orim2i 762	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 133	. . 3 |- ( ps -> ph )
5	4	orim2i 762	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 126	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Syntax hints:   <-> wb 105   \/ wo 709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  764  orbi12i  765  orass  768  or4  772  or42  773  orordir  775  dcnnOLD  850  orbididc  955  3orcomb  989  excxor  1389  xordc  1403  nf4dc  1681  nf4r  1682  19.44  1693  dveeq2  1826  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  dcne  2375  unass  3316  undi  3407  undif3ss  3420  symdifxor  3425  undif4  3509  iinuniss  3995  ordsucim  4532  suc11g  4589  qfto  5055  nntri3or  6546  reapcotr  8617  elnn0  9242  elxnn0  9305  elnn1uz2  9672  nn01to3  9682  elxr  9842  xaddcom  9927  xnegdi  9934  xpncan  9937  xleadd1a  9939  lcmdvds  12217  mulgcddvds  12232  cncongr2  12242  pythagtrip  12421  bj-peano4  15447  apdifflemr  15537