Theorem orcom 246

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		bi2.15 166	. 2 |- ((-. ph -> ps) <-> (-. ps -> ph))
2		df-or 224	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3		df-or 224	. 2 |- ((ps \/ ph) <-> (-. ps -> ph))
4	1, 2, 3	3bitr4 183	1 |- ((ph \/ ps) <-> (ps \/ ph))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 146   \/ wo 222

This theorem is referenced by:  pm1.4 247  orel2 252  orbi1i 256  orass 260  or23 263  or42 265  ordir 595  orbi1d 613  pm5.17 666  xor 669  pm5.55 673  biorfi 734  pm5.7 744  ecase2d 749  prlem2 769  3orrot 779  19.30 1081  19.31 1083  19.33b 1088  mooran2 1419  euor2 1430  eueq2 1909  eueq3 1910  uncom 2166  symdif2 2256  reuun2 2268  dfif2 2353  difprsn 2456  prel12 2475  zfpair 2767  pwssun 2816  dfwe2 2925  ordtri1 2970  ordtri2 2972  ordtri2or 3067  ordunisuc2 3105  on0eqelt 3114  fununi 3549  dfrdg2 3918  suplem2pr 5134  ltxrltt 5472  leloet 5491  xrleloet 5530  xrrebndt 5541  arch 6018  xrsupss 6025  elznn0nn 6095  elznn0 6096  nneo 6144  icounlem 6345  snunioolem 6347  elfzp1 6442  sqeqor 6578  absgt0 6778  pilem1 8590  hvmulcan2t 8861  elat2 10175  chrelat2 10200  atoml2 10218

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