![]() |
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 723 | . 2 ⊢ ((𝜓 ∨ 𝜒) → (¬ 𝜓 → 𝜒)) | |
3 | 1, 2 | syl 14 | 1 ⊢ (𝜑 → (¬ 𝜓 → 𝜒)) |
Colors of variables: wff set class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 709 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in2 616 ax-io 710 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm2.8 811 orcanai 929 ax12 1523 swopo 4321 sotritrieq 4340 suc11g 4571 ordsoexmid 4576 nnsuc 4630 sotri2 5041 nnsucsssuc 6511 nntri2 6513 nntri1 6515 nnsseleq 6520 djulclb 7072 0ct 7124 exmidomniim 7157 omniwomnimkv 7183 elni2 7331 nlt1pig 7358 nngt1ne1 8972 zleloe 9318 zapne 9345 nneo 9374 zeo2 9377 fzocatel 10217 dfphi2 12238 prmdiv 12253 odzdvds 12263 pc2dvds 12347 fldivp1 12364 pcfac 12366 1arith 12383 4sqlem10 12403 lgseisenlem1 14847 bj-peano4 15104 |
Copyright terms: Public domain | W3C validator |