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 599  orbi1d 617  pm5.17 670  xor 673  pm5.55 677  biorfi 738  pm5.7 748  ecase2d 753  prlem2 773  3orrot 783  19.30 1087  19.31 1089  19.33b 1094  mooran2 1428  euor2 1440  eueq2 1921  eueq3 1922  uncom 2179  symdif2 2269  reuun2 2281  dfif2 2367  difprsn 2469  prel12 2488  zfpair 2783  pwssun 2833  dfwe2 2941  ordtri1 2986  ordtri2 2988  ordtri2or 3083  ordunisuc2 3121  on0eqelt 3130  fununi 3569  dfrdg2 3939  suplem2pr 5174  ltxrltt 5512  leloet 5530  xrleloet 5569  xrrebndt 5580  arch 6073  xrsupss 6080  elznn0nn 6150  elznn0 6151  nneo 6199  icounlem 6413  snunioolem 6415  elfzp1 6511  sqeqor 6648  pilem1 8666  hvmulcan2t 8935  elat2 10262  chrelat2 10287  atoml2 10305

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