New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > orcom | GIF version |
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.) |
Ref | Expression |
---|---|
orcom | ⊢ ((φ ∨ ψ) ↔ (ψ ∨ φ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm1.4 375 | . 2 ⊢ ((φ ∨ ψ) → (ψ ∨ φ)) | |
2 | pm1.4 375 | . 2 ⊢ ((ψ ∨ φ) → (φ ∨ ψ)) | |
3 | 1, 2 | impbii 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 |