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  1694  nf4r  1695  19.44  1706  dveeq2  1839  dvelimALT  2039  dvelimfv  2040  dvelimor  2047  dcne  2389  unass  3338  undi  3429  undif3ss  3442  symdifxor  3447  undif4  3531  iinuniss  4024  ordsucim  4566  suc11g  4623  qfto  5091  nntri3or  6602  reapcotr  8706  elnn0  9332  elxnn0  9395  elnn1uz2  9763  nn01to3  9773  elxr  9933  xaddcom  10018  xnegdi  10025  xpncan  10028  xleadd1a  10030  lcmdvds  12516  mulgcddvds  12531  cncongr2  12541  pythagtrip  12721  bj-peano4  16090  apdifflemr  16188