Theorem orbi2i 774

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

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

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 721

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  775  orbi12i  776  orass  779  or4  783  or42  784  orordir  786  dcnnOLD  861  orbididc  966  3orcomb  1018  excxor  1427  xordc  1441  nf4dc  1722  nf4r  1723  19.44  1734  dveeq2  1868  dvelimALT  2070  dvelimfv  2071  dvelimor  2078  dcne  2431  unass  3386  undi  3479  undif3ss  3492  symdifxor  3497  undif4  3586  iinuniss  4090  ordsucim  4642  suc11g  4699  qfto  5172  nntri3or  6756  reapcotr  8916  elnn0  9544  elxnn0  9611  elnn1uz2  9986  nn01to3  9996  elxr  10157  xaddcom  10242  xnegdi  10249  xpncan  10252  xleadd1a  10254  hashf1lem2  11264  lcmdvds  12835  mulgcddvds  12850  cncongr2  12860  pythagtrip  13040  bj-peano4  16895  apdifflemr  17001