![]() |
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 674 | . 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 662 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 ax-in2 578 ax-io 663 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: pm2.8 757 orcanai 871 ax-12 1443 swopo 4096 sotritrieq 4115 suc11g 4335 ordsoexmid 4340 nnsuc 4392 sotri2 4783 nnsucsssuc 6184 nntri2 6186 nntri1 6188 nnsseleq 6193 djulclb 6653 exmidomniim 6701 elni2 6775 nlt1pig 6802 nngt1ne1 8349 zleloe 8692 zapne 8716 nneo 8744 zeo2 8747 fzocatel 9498 dfphi2 10975 bj-peano4 11192 |
Copyright terms: Public domain | W3C validator |