Theorem orbi2i 769

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  orbi1i  770  orbi12i  771  orass  774  or4  778  or42  779  orordir  781  dcnnOLD  856  orbididc  961  3orcomb  1013  excxor  1422  xordc  1436  nf4dc  1718  nf4r  1719  19.44  1730  dveeq2  1863  dvelimALT  2063  dvelimfv  2064  dvelimor  2071  dcne  2413  unass  3364  undi  3455  undif3ss  3468  symdifxor  3473  undif4  3557  iinuniss  4053  ordsucim  4598  suc11g  4655  qfto  5126  nntri3or  6660  reapcotr  8777  elnn0  9403  elxnn0  9466  elnn1uz2  9840  nn01to3  9850  elxr  10010  xaddcom  10095  xnegdi  10102  xpncan  10105  xleadd1a  10107  lcmdvds  12650  mulgcddvds  12665  cncongr2  12675  pythagtrip  12855  bj-peano4  16550  apdifflemr  16651