Theorem orbi2i 757

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 119	. . 3 |- ( ph -> ps )
3	2	orim2i 756	. 2 |- ( ( ch \/ ph ) -> ( ch \/ ps ) )
4	1	biimpri 132	. . 3 |- ( ps -> ph )
5	4	orim2i 756	. 2 |- ( ( ch \/ ps ) -> ( ch \/ ph ) )
6	3, 5	impbii 125	1 |- ( ( ch \/ ph ) <-> ( ch \/ ps ) )

Syntax hints:   <-> wb 104   \/ wo 703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 704

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  758  orbi12i  759  orass  762  or4  766  or42  767  orordir  769  dcnnOLD  844  orbididc  948  3orcomb  982  excxor  1373  xordc  1387  nf4dc  1663  nf4r  1664  19.44  1675  dveeq2  1808  dvelimALT  2003  dvelimfv  2004  dvelimor  2011  dcne  2351  unass  3284  undi  3375  undif3ss  3388  symdifxor  3393  undif4  3477  iinuniss  3955  ordsucim  4484  suc11g  4541  qfto  5000  nntri3or  6472  reapcotr  8517  elnn0  9137  elxnn0  9200  elnn1uz2  9566  nn01to3  9576  elxr  9733  xaddcom  9818  xnegdi  9825  xpncan  9828  xleadd1a  9830  lcmdvds  12033  mulgcddvds  12048  cncongr2  12058  pythagtrip  12237  bj-peano4  13990  apdifflemr  14079