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  2523  r19.30  2757  sspsstri  3372  unass  3421  undi  3503  undif3  3516  undif4  3608  ssunpr  3869  sspr  3870  sstp  3871  iinun2  4033  iinuni  4050  axtyplowerprim  4095  pwadjoin  4120  nnsucelrlem2  4426  ltfintrilem1  4466  nnadjoin  4521  dfphi2  4570  phi011lem1  4599  clos1baseima  5884  clos1basesucg  5885  fce  6189