Theorem orbi2i 763

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

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

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 710

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  764  orbi12i  765  orass  768  or4  772  or42  773  orordir  775  dcnnOLD  850  orbididc  955  3orcomb  989  excxor  1389  xordc  1403  nf4dc  1681  nf4r  1682  19.44  1693  dveeq2  1826  dvelimALT  2026  dvelimfv  2027  dvelimor  2034  dcne  2375  unass  3317  undi  3408  undif3ss  3421  symdifxor  3426  undif4  3510  iinuniss  3996  ordsucim  4533  suc11g  4590  qfto  5056  nntri3or  6548  reapcotr  8619  elnn0  9245  elxnn0  9308  elnn1uz2  9675  nn01to3  9685  elxr  9845  xaddcom  9930  xnegdi  9937  xpncan  9940  xleadd1a  9942  lcmdvds  12220  mulgcddvds  12235  cncongr2  12245  pythagtrip  12424  bj-peano4  15517  apdifflemr  15607