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  4649  suc11g  4706  qfto  5180  nntri3or  6770  reapcotr  8934  elnn0  9576  elxnn0  9643  elnn1uz2  10023  nn01to3  10033  elxr  10195  xaddcom  10280  xnegdi  10287  xpncan  10290  xleadd1a  10292  hashf1lem2  11308  lcmdvds  12882  mulgcddvds  12897  cncongr2  12907  pythagtrip  13091  bj-peano4  17186  apdifflemr  17303