Theorem orbi12i 507

Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
orbi12i.1	|- (ph <-> ps)
orbi12i.2	|- (ch <-> th)

Assertion

Ref	Expression
orbi12i	|- ((ph \/ ch) <-> (ps \/ th))

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 |- (ch <-> th)
2	1	orbi2i 505	. 2 |- ((ph \/ ch) <-> (ph \/ th))
3		orbi12i.1	. . 3 |- (ph <-> ps)
4	3	orbi1i 506	. 2 |- ((ph \/ th) <-> (ps \/ th))
5	2, 4	bitri 240	1 |- ((ph \/ ch) <-> (ps \/ th))

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:  pm4.78  565  andir  838  anddi  840  dfbi3  863  4exmid  905  3orbi123i  1141  3or6  1263  cadcoma  1395  neorian  2604  elsymdif  3224  sspsstri  3372  rexun  3444  indi  3502  symdif2  3521  unab  3522  inundif  3629  elimif  3692  dfpr2  3750  ssunsn  3867  ssunpr  3869  sspr  3870  sstp  3871  pwpr  3884  pwtp  3885  unipr  3906  uniun  3911  iunun  4047  iunxun  4048  axprimlem2  4090  axsiprim  4094  axins2prim  4096  axins3prim  4097  pwadjoin  4120  pw1un  4164  dfaddc2  4382  nnsucelrlem1  4425  nndisjeq  4430  ltfinex  4465  ltfintrilem1  4466  eqtfinrelk  4487  evenfinex  4504  oddfinex  4505  evenodddisjlem1  4516  nnadjoinlem1  4520  vfinspss  4552  dfphi2  4570  dfop2lem1  4574  proj1op  4601  proj2op  4602  eqop  4612  brun  4693  setconslem2  4733  setconslem3  4734  setconslem7  4738  dfswap2  4742  dmun  4913  xpeq0  5047  cupex  5817  connexex  5914  enprmaplem4  6080  leconnnc  6219  nmembers1lem3  6271  nncdiv3lem2  6277  nchoicelem16  6305  nchoicelem17  6306  nchoicelem18  6307