Theorem orbi12i 264

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 262	. 2 |- ((ph \/ ch) <-> (ph \/ th))
3		orbi12i.1	. . 3 |- (ph <-> ps)
4	3	orbi1i 263	. 2 |- ((ph \/ th) <-> (ps \/ th))
5	2, 4	bitri 180	1 |- ((ph \/ ch) <-> (ps \/ th))

Syntax hints:   <-> wb 153   \/ wo 229

This theorem is referenced by:  ioran 313  pm4.79 362  andir 616  anddi 618  xor 682  pm5.55 687  consensus 779  prlem2 783  3orbi123i 835  19.33b 1133  neorian 1687  r19.43 1812  sspsstri 2199  indi 2302  symdif2 2317  unab 2318  elimif 2426  dfpr2 2474  eltp 2491  unipr 2569  uniun 2573  iunxun 2669  zfpair 2833  pwunss 2882  pwundif 2884  opthprc 3278  dmun 3374  cnvun 3512  xpeq0 3524  dfrdg2 3991  oarec 4254  brdom2 4449  kmlem16 4842  ltsor 5326  ssxr 5605  lesubaddi 5660  lenegi 5669  elnn0z 6229  elnn0nn 6253  icounlem 6438  snunioolem 6440  sqeqori 6736  usinuniop 10703

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 154  df-or 231

Copyright terms: Public domain