Theorem orbi2i 752

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

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

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  orbi1i  753  orbi12i  754  orass  757  or4  761  or42  762  orordir  764  dcnnOLD  835  orbididc  938  3orcomb  972  excxor  1360  xordc  1374  nf4dc  1650  nf4r  1651  19.44  1662  dveeq2  1795  dvelimALT  1990  dvelimfv  1991  dvelimor  1998  dcne  2338  unass  3264  undi  3355  undif3ss  3368  symdifxor  3373  undif4  3456  iinuniss  3931  ordsucim  4458  suc11g  4515  qfto  4974  nntri3or  6437  reapcotr  8467  elnn0  9086  elxnn0  9149  elnn1uz2  9511  nn01to3  9519  elxr  9676  xaddcom  9758  xnegdi  9765  xpncan  9768  xleadd1a  9770  lcmdvds  11947  mulgcddvds  11962  cncongr2  11972  bj-peano4  13501  apdifflemr  13589