Theorem orbi2i 505

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 186	. . 3 |- (ph -> ps)
3	2	orim2i 504	. 2 |- ((ch \/ ph) -> (ch \/ ps))
4	1	biimpri 197	. . 3 |- (ps -> ph)
5	4	orim2i 504	. 2 |- ((ch \/ ps) -> (ch \/ ph))
6	3, 5	impbii 180	1 |- ((ch \/ ph) <-> (ch \/ ps))

Syntax hints:   <-> wb 176   \/ wo 357

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 177  df-or 359

This theorem is referenced by:  orbi1i  506  orbi12i  507  orass  510  or4  514  or42  515  orordir  517  dn1  932  3orcomb  944  excxor  1309  cad1  1398  nf4  1868  19.44  1877  exmidne  2522  r19.30  2756  sspsstri  3371  unass  3420  undi  3502  undif3  3515  undif4  3607  ssunpr  3868  sspr  3869  sstp  3870  iinun2  4032  iinuni  4049  axtyplowerprim  4094  pwadjoin  4119  nnsucelrlem2  4425  ltfintrilem1  4465  nnadjoin  4520  dfphi2  4569  phi011lem1  4598  clos1baseima  5883  clos1basesucg  5884  fce  6188