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  3361  undi  3452  undif3ss  3465  symdifxor  3470  undif4  3554  iinuniss  4048  ordsucim  4592  suc11g  4649  qfto  5118  nntri3or  6639  reapcotr  8745  elnn0  9371  elxnn0  9434  elnn1uz2  9802  nn01to3  9812  elxr  9972  xaddcom  10057  xnegdi  10064  xpncan  10067  xleadd1a  10069  lcmdvds  12601  mulgcddvds  12616  cncongr2  12626  pythagtrip  12806  bj-peano4  16318  apdifflemr  16415