Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > intnand | Unicode version |
Description: Introduction of conjunct inside of a contradiction. (Contributed by NM, 10-Jul-2005.) |
Ref | Expression |
---|---|
intnand.1 |
Ref | Expression |
---|---|
intnand |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | intnand.1 | . 2 | |
2 | simpr 109 | . 2 | |
3 | 1, 2 | nsyl 602 | 1 |
Colors of variables: wff set class |
Syntax hints: wn 3 wi 4 wa 103 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-in1 588 ax-in2 589 |
This theorem is referenced by: dcan 903 poxp 6097 cauappcvgprlemladdrl 7433 caucvgprlemladdrl 7454 xrrebnd 9570 fzpreddisj 9819 fzp1nel 9852 gcdsupex 11573 gcdsupcl 11574 gcdnncl 11583 gcd2n0cl 11585 qredeu 11705 cncongr2 11712 divnumden 11801 divdenle 11802 ivthinclemdisj 12714 |
Copyright terms: Public domain | W3C validator |