Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ord | GIF version |
Description: Deduce implication from disjunction. (Contributed by NM, 18-May-1994.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
ord.1 | ⊢ (𝜑 → (𝜓 ∨ 𝜒)) |
Ref | Expression |
---|---|
ord | ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ord.1 | . 2 ⊢ (𝜑 → (𝜓 ∨ 𝜒)) | |
2 | pm2.53 712 | . 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 698 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in2 605 ax-io 699 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.8 800 orcanai 914 ax12 1492 swopo 4269 sotritrieq 4288 suc11g 4519 ordsoexmid 4524 nnsuc 4578 sotri2 4986 nnsucsssuc 6442 nntri2 6444 nntri1 6446 nnsseleq 6451 djulclb 7002 0ct 7054 exmidomniim 7087 omniwomnimkv 7113 elni2 7237 nlt1pig 7264 nngt1ne1 8874 zleloe 9220 zapne 9244 nneo 9273 zeo2 9276 fzocatel 10108 dfphi2 12111 prmdiv 12126 odzdvds 12136 bj-peano4 13627 |
Copyright terms: Public domain | W3C validator |