Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ord | Unicode 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 918 ax12 1499 swopo 4278 sotritrieq 4297 suc11g 4528 ordsoexmid 4533 nnsuc 4587 sotri2 4995 nnsucsssuc 6451 nntri2 6453 nntri1 6455 nnsseleq 6460 djulclb 7011 0ct 7063 exmidomniim 7096 omniwomnimkv 7122 elni2 7246 nlt1pig 7273 nngt1ne1 8883 zleloe 9229 zapne 9256 nneo 9285 zeo2 9288 fzocatel 10124 dfphi2 12131 prmdiv 12146 odzdvds 12156 pc2dvds 12240 fldivp1 12257 pcfac 12259 bj-peano4 13678 |
Copyright terms: Public domain | W3C validator |