Theorem orbi2i 762

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

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

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 709

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  763  orbi12i  764  orass  767  or4  771  or42  772  orordir  774  dcnnOLD  849  orbididc  953  3orcomb  987  excxor  1378  xordc  1392  nf4dc  1670  nf4r  1671  19.44  1682  dveeq2  1815  dvelimALT  2010  dvelimfv  2011  dvelimor  2018  dcne  2358  unass  3293  undi  3384  undif3ss  3397  symdifxor  3402  undif4  3486  iinuniss  3970  ordsucim  4500  suc11g  4557  qfto  5019  nntri3or  6494  reapcotr  8555  elnn0  9178  elxnn0  9241  elnn1uz2  9607  nn01to3  9617  elxr  9776  xaddcom  9861  xnegdi  9868  xpncan  9871  xleadd1a  9873  lcmdvds  12079  mulgcddvds  12094  cncongr2  12104  pythagtrip  12283  bj-peano4  14710  apdifflemr  14798