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  6647  reapcotr  8756  elnn0  9382  elxnn0  9445  elnn1uz2  9814  nn01to3  9824  elxr  9984  xaddcom  10069  xnegdi  10076  xpncan  10079  xleadd1a  10081  lcmdvds  12617  mulgcddvds  12632  cncongr2  12642  pythagtrip  12822  bj-peano4  16401  apdifflemr  16503