Theorem orbi2i 770

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

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  771  orbi12i  772  orass  775  or4  779  or42  780  orordir  782  dcnnOLD  857  orbididc  962  3orcomb  1014  excxor  1423  xordc  1437  nf4dc  1718  nf4r  1719  19.44  1730  dveeq2  1864  dvelimALT  2066  dvelimfv  2067  dvelimor  2074  dcne  2425  unass  3380  undi  3473  undif3ss  3486  symdifxor  3491  undif4  3575  iinuniss  4079  ordsucim  4627  suc11g  4684  qfto  5157  nntri3or  6739  reapcotr  8889  elnn0  9515  elxnn0  9582  elnn1uz2  9957  nn01to3  9967  elxr  10128  xaddcom  10213  xnegdi  10220  xpncan  10223  xleadd1a  10225  lcmdvds  12801  mulgcddvds  12816  cncongr2  12826  pythagtrip  13006  bj-peano4  16851  apdifflemr  16957