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 696 | . 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 682 |
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 589 ax-io 683 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.8 784 orcanai 898 ax-12 1474 swopo 4198 sotritrieq 4217 suc11g 4442 ordsoexmid 4447 nnsuc 4499 sotri2 4906 nnsucsssuc 6356 nntri2 6358 nntri1 6360 nnsseleq 6365 djulclb 6908 0ct 6960 exmidomniim 6981 elni2 7090 nlt1pig 7117 nngt1ne1 8723 zleloe 9069 zapne 9093 nneo 9122 zeo2 9125 fzocatel 9944 dfphi2 11823 bj-peano4 13080 |
Copyright terms: Public domain | W3C validator |