Theorem orbi12i 277

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

Syntax hints:   <-> wb 163   \/ wo 239

This theorem is referenced by:  ioranOLD 332  pm4.79 382  andir 666  anddi 668  xor 734  pm5.55 739  consensusOLD 845  prlem2OLD 851  3orbi123i 1057  19.33bOLD 1445  neorian 2098  r19.43OLD 2239  unjustOLD 2599  sspsstri 2711  rexun 2783  indi 2838  indiOLD 2839  symdif2 2857  symdif2OLD 2858  unab 2859  unabOLD 2860  inundif 2951  elimif 3001  dfpr2 3059  eltp 3074  pwpr 3174  unipr 3191  uniun 3196  iunxun 3329  brun 3387  zfpair 3522  pwunss 3577  pwundif 3579  opthprc 4046  dmunOLD 4164  cnvunOLD 4323  xpeq0 4336  coundiOLD 4397  coundirOLD 4399  dfrdg2 5141  oarec 5244  brdom2 5447  kmlem16 5942  ltsor 6413  ssxrOLD 6715  lesubaddiOLD 6772  lenegi 6784  elnn0z 7356  elnn0nn 7380  icounlem 7581  snunioolem 7583  sqeqori 7893  elfilmap 10312  usinuniop 10341  bnj1394 13108  bnj1406 13116  bnj1427 13121  3or6 13804  nepss 13820  dfon2lem4 13852  dfon2lem5 13853  elsymdif 14062  dfon3 14072  anddi2 14268  tostos 14637  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  locfincomp 15514  filssufillem 15570  cnpfillim 15589  rexunOLD 15656  fzsplit 15792  ispridl2 16186  smprngpr 16200  isdmn3 16222  elpadd 17260  paddasslem17 17297

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 164  df-or 241

Copyright terms: Public domain