Theorem orbi12i 257

Description: Infer the disjunction of two equivalences.

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 255	. 2 |- ((ph \/ ch) <-> (ph \/ th))
3		orbi12i.1	. . 3 |- (ph <-> ps)
4	3	orbi1i 256	. 2 |- ((ph \/ th) <-> (ps \/ th))
5	2, 4	bitr 173	1 |- ((ph \/ ch) <-> (ps \/ th))

Syntax hints:   <-> wb 146   \/ wo 222

This theorem is referenced by:  ioran 306  pm4.79 355  andir 604  anddi 606  xor 670  pm5.55 674  consensus 766  prlem2 770  3orbi123i 822  19.33b 1090  neorian 1637  r19.43 1762  sspsstri 2144  indi 2247  symdif2 2262  unab 2263  elimif 2370  dfpr2 2418  eltp 2435  unipr 2510  uniun 2514  iunxun 2609  zfpair 2772  pwunss 2821  pwundif 2823  opthprc 3216  dmun 3312  cnvun 3447  xpeq0 3459  dfrdg2 3924  oarec 4186  brdom2 4375  kmlem16 4760  ltsor 5241  ssxr 5521  lesubadd 5577  leneg 5586  elnn0z 6102  elnn0nn 6126  icounlem 6353  snunioolem 6355  sqeqor 6586

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

This theorem depends on definitions:  df-bi 147  df-or 224

Copyright terms: Public domain