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  2603  elsymdif  3223  sspsstri  3371  rexun  3443  indi  3501  symdif2  3520  unab  3521  inundif  3628  elimif  3691  dfpr2  3749  ssunsn  3866  ssunpr  3868  sspr  3869  sstp  3870  pwpr  3883  pwtp  3884  unipr  3905  uniun  3910  iunun  4046  iunxun  4047  axprimlem2  4089  axsiprim  4093  axins2prim  4095  axins3prim  4096  pwadjoin  4119  pw1un  4163  dfaddc2  4381  nnsucelrlem1  4424  nndisjeq  4429  ltfinex  4464  ltfintrilem1  4465  eqtfinrelk  4486  evenfinex  4503  oddfinex  4504  evenodddisjlem1  4515  nnadjoinlem1  4519  vfinspss  4551  dfphi2  4569  dfop2lem1  4573  proj1op  4600  proj2op  4601  eqop  4611  brun  4692  setconslem2  4732  setconslem3  4733  setconslem7  4737  dfswap2  4741  dmun  4912  xpeq0  5046  cupex  5816  connexex  5913  enprmaplem4  6079  leconnnc  6218  nmembers1lem3  6270  nncdiv3lem2  6276  nchoicelem16  6304  nchoicelem17  6305  nchoicelem18  6306