NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  orcom GIF version

Theorem orcom 376
Description: Commutative law for disjunction. Theorem *4.31 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 15-Nov-2012.)
Assertion
Ref Expression
orcom ((φ ψ) ↔ (ψ φ))

Proof of Theorem orcom
StepHypRef Expression
1 pm1.4 375 . 2 ((φ ψ) → (ψ φ))
2 pm1.4 375 . 2 ((ψ φ) → (φ ψ))
31, 2impbii 180 1 ((φ ψ) ↔ (ψ φ))
Colors of variables: wff setvar class
Syntax hints:  wb 176   wo 357
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8
This theorem depends on definitions:  df-bi 177  df-or 359
This theorem is referenced by:  orcomd  377  orbi1i  506  orass  510  or32  513  or42  515  orbi1d  683  pm5.61  693  oranabs  829  ordir  835  pm5.17  858  pm5.7  900  pm5.75  903  dn1  932  3orrot  940  3orcomb  944  cadan  1392  nf4  1868  19.31  1876  r19.30  2756  eueq2  3010  uncom  3408  reuun2  3538  dfif2  3664  ssunsn2  3865  ltfintri  4466  evenoddnnnul  4514  dfphi2  4569  proj2op  4601  fununi  5160  fce  6188
  Copyright terms: Public domain W3C validator