Theorem orbi2i 767

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  768  orbi12i  769  orass  772  or4  776  or42  777  orordir  779  dcnnOLD  854  orbididc  959  3orcomb  1011  excxor  1420  xordc  1434  nf4dc  1716  nf4r  1717  19.44  1728  dveeq2  1861  dvelimALT  2061  dvelimfv  2062  dvelimor  2069  dcne  2411  unass  3362  undi  3453  undif3ss  3466  symdifxor  3471  undif4  3555  iinuniss  4049  ordsucim  4594  suc11g  4651  qfto  5122  nntri3or  6654  reapcotr  8766  elnn0  9392  elxnn0  9455  elnn1uz2  9829  nn01to3  9839  elxr  9999  xaddcom  10084  xnegdi  10091  xpncan  10094  xleadd1a  10096  lcmdvds  12638  mulgcddvds  12653  cncongr2  12663  pythagtrip  12843  bj-peano4  16460  apdifflemr  16561