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  4548  suc11g  4605  qfto  5072  nntri3or  6579  reapcotr  8671  elnn0  9297  elxnn0  9360  elnn1uz2  9728  nn01to3  9738  elxr  9898  xaddcom  9983  xnegdi  9990  xpncan  9993  xleadd1a  9995  lcmdvds  12401  mulgcddvds  12416  cncongr2  12426  pythagtrip  12606  bj-peano4  15891  apdifflemr  15986