Theorem orcom 266

Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118.

Assertion

Ref	Expression
orcom	|- ((ph \/ ps) <-> (ps \/ ph))

Proof of Theorem orcom

Step	Hyp	Ref	Expression
1		con1b 181	. 2 |- ((-. ph -> ps) <-> (-. ps -> ph))
2		df-or 241	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3		df-or 241	. 2 |- ((ps \/ ph) <-> (-. ps -> ph))
4	1, 2, 3	3bitr4i 200	1 |- ((ph \/ ps) <-> (ps \/ ph))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 163   \/ wo 239

This theorem is referenced by:  pm1.4 267  orel2 272  orbi1i 276  orass 280  orassOLD 281  or23 284  or23OLD 285  or42 287  ordir 658  orbi1d 677  pm5.17 731  xor 734  pm5.55 739  biorfi 808  pm5.7 818  ecase2d 824  prlem2OLD 851  3orrot 864  3orcomb 867  19.30OLD 1437  19.31 1439  19.33bOLD 1445  mooran2OLD 1825  euor2OLD 1840  eueq2 2429  eueq3 2430  uncom 2744  uncomOLD 2745  symdif2OLD 2858  reuun2 2873  dfif2 2984  difprsnOLD 3128  prel12 3155  zfpair 3522  pwssun 3578  ordtri1OLD 3694  ordtri2 3696  ordtri2orOLD 3767  on0eqel 3787  dfwe2OLD 3862  ordunisuc2 3926  dfco2aOLD 4395  fununi 4481  dfrdg2 5141  suplem2pr 6314  ltxrlt 6669  leloe 6688  xrleloe 6732  xrrebnd 6743  arch 7280  xrsupss 7287  elznn0nn 7357  elznn0 7358  nneoi 7409  icounlem 7581  snunioolem 7583  elfzp1 7683  sqeqori 7893  pilem1 10020  hvmulcan2 10573  elat2 11912  chrelat2i 11937  atoml2i 11955  bnj559 12539  elnn00nn 13602  coprm 13782  3orel2 13806  r19.30 13817  dfon2lem5 13853  axfelem8 14038  dutos1 14626  intartar 15255  vtarsuelt 15272  ecase13d 15350  elicc3 15362  subntr 15425  alexsublem2 15438  alexsublem3 15439  alexsublem4 15440  isufil2 15565  filcon 15580  fimaxre 15774  fzm1 15796  pleval2 16785  leatom 17005  hlrelat2 17052  elpadd0 17270

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