![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > orcomd | GIF version |
Description: Commutation of disjuncts in consequent. (Contributed by NM, 2-Dec-2010.) |
Ref | Expression |
---|---|
orcomd.1 | ⊢ (φ → (ψ ∨ χ)) |
Ref | Expression |
---|---|
orcomd | ⊢ (φ → (χ ∨ ψ)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | orcomd.1 | . 2 ⊢ (φ → (ψ ∨ χ)) | |
2 | orcom 646 | . 2 ⊢ ((ψ ∨ χ) ↔ (χ ∨ ψ)) | |
3 | 1, 2 | sylib 127 | 1 ⊢ (φ → (χ ∨ ψ)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∨ wo 628 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: olcd 652 stabtestimpdc 823 pm5.54dc 826 swopo 4034 sotritrieq 4053 acexmidlemcase 5450 2oconcl 5961 nntri3or 6011 nntri2 6012 nntri1 6013 addnqprlemfu 6541 addcanprlemu 6589 cauappcvgprlemladdru 6628 apreap 7371 mulap0r 7399 nnm1nn0 7999 elnn0z 8034 zleloe 8068 nneoor 8116 nneo 8117 zeo2 8120 uzm1 8279 nn01to3 8328 uzsplit 8724 fzospliti 8802 fzouzsplit 8805 |
Copyright terms: Public domain | W3C validator |