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  1684  nf4r  1685  19.44  1696  dveeq2  1829  dvelimALT  2029  dvelimfv  2030  dvelimor  2037  dcne  2378  unass  3321  undi  3412  undif3ss  3425  symdifxor  3430  undif4  3514  iinuniss  4000  ordsucim  4537  suc11g  4594  qfto  5060  nntri3or  6560  reapcotr  8642  elnn0  9268  elxnn0  9331  elnn1uz2  9698  nn01to3  9708  elxr  9868  xaddcom  9953  xnegdi  9960  xpncan  9963  xleadd1a  9965  lcmdvds  12272  mulgcddvds  12287  cncongr2  12297  pythagtrip  12477  bj-peano4  15685  apdifflemr  15778