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 ) )

This proof depends on syntax axioms:   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used 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  3587  iinuniss  4095  ordsucim  4647  suc11g  4704  qfto  5177  nntri3or  6766  reapcotr  8928  elnn0  9569  elxnn0  9636  elnn1uz2  10016  nn01to3  10026  elxr  10188  xaddcom  10273  xnegdi  10280  xpncan  10283  xleadd1a  10285  hashf1lem2  11300  lcmdvds  12873  mulgcddvds  12888  cncongr2  12898  pythagtrip  13082  bj-peano4  17079  apdifflemr  17194