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 717 | . 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 703 |
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 610 ax-io 704 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm2.8 805 orcanai 923 ax12 1505 swopo 4291 sotritrieq 4310 suc11g 4541 ordsoexmid 4546 nnsuc 4600 sotri2 5008 nnsucsssuc 6471 nntri2 6473 nntri1 6475 nnsseleq 6480 djulclb 7032 0ct 7084 exmidomniim 7117 omniwomnimkv 7143 elni2 7276 nlt1pig 7303 nngt1ne1 8913 zleloe 9259 zapne 9286 nneo 9315 zeo2 9318 fzocatel 10155 dfphi2 12174 prmdiv 12189 odzdvds 12199 pc2dvds 12283 fldivp1 12300 pcfac 12302 1arith 12319 4sqlem10 12339 bj-peano4 13990 |
Copyright terms: Public domain | W3C validator |