![]() |
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 640 | . 2 ⊢ ((ψ ∨ χ) → (¬ ψ → χ)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (φ → (¬ ψ → χ)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → 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-in2 545 ax-io 629 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: pm2.8 722 orcanai 836 ax-12 1399 swopo 4034 sotritrieq 4053 suc11g 4235 ordsoexmid 4240 nnsuc 4281 sotri2 4665 nnsucsssuc 6010 nntri2 6012 nntri1 6013 elni2 6298 nlt1pig 6325 nngt1ne1 7729 zleloe 8068 zapne 8091 nneo 8117 zeo2 8120 fzocatel 8825 bj-peano4 9415 |
Copyright terms: Public domain | W3C validator |