Theorem orcom 209

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 145	. 2 |- ((-. ph -> ps) <-> (-. ps -> ph))
2		df-or 197	. 2 |- ((ph \/ ps) <-> (-. ph -> ps))
3		df-or 197	. 2 |- ((ps \/ ph) <-> (-. ps -> ph))
4	1, 2, 3	3bitr4 158	1 |- ((ph \/ ps) <-> (ps \/ ph))

Syntax hints:  -. wn 1   -> wi 2   <-> wb 127   \/ wo 195

This theorem is referenced by:  orel2 213  orbi1i 215  orass 218  or23 219  or42 221  ordir 453  orbi1d 467  xor 500  biorfi 552  ecase2d 558  prlem2 577  3orrot 587  19.30 764  19.31 766  19.33b 771  mooran2 1050  eueq2 1429  eueq3 1430  uncom 1604  symdif2 1690  prel12 1875  zfpair 1891  pwssun 1917  dfwe2 2187  ordsseleq 2227  ordtri1 2231  ordtri2 2233  ordtri2or 2328  on0eqelt 2370  fununi 2705  suplem2pr 3956  leloet 4284  arch 4521  elznn0nn 4575  elznn0 4576  nneo 4719  absgt0 4842  elat2 5739  chrelat2 5758

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-or 197

metamath.org