Theorem orbi2i 764

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

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

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 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  765  orbi12i  766  orass  769  or4  773  or42  774  orordir  776  dcnnOLD  851  orbididc  956  3orcomb  990  excxor  1398  xordc  1412  nf4dc  1693  nf4r  1694  19.44  1705  dveeq2  1838  dvelimALT  2038  dvelimfv  2039  dvelimor  2046  dcne  2387  unass  3330  undi  3421  undif3ss  3434  symdifxor  3439  undif4  3523  iinuniss  4010  ordsucim  4549  suc11g  4606  qfto  5073  nntri3or  6581  reapcotr  8673  elnn0  9299  elxnn0  9362  elnn1uz2  9730  nn01to3  9740  elxr  9900  xaddcom  9985  xnegdi  9992  xpncan  9995  xleadd1a  9997  lcmdvds  12434  mulgcddvds  12449  cncongr2  12459  pythagtrip  12639  bj-peano4  15928  apdifflemr  16023