| 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 110 |
. 2
| |
| 3 | 1, 2 | nsyl 633 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-in1 619 ax-in2 620 |
| This theorem is referenced by: dcand 941 poxp 6442 cauappcvgprlemladdrl 7989 caucvgprlemladdrl 8010 xrrebnd 10175 fzpreddisj 10431 fzp1nel 10464 fprodntrivap 12300 bitsfzo 12671 bitsmod 12672 gcdsupex 12683 gcdsupcl 12684 gcdnncl 12693 gcd2n0cl 12695 qredeu 12824 cncongr2 12831 divnumden 12923 divdenle 12924 phisum 12968 pythagtriplem4 12996 pythagtriplem8 13000 pythagtriplem9 13001 isnsgrp 13674 ivthinclemdisj 15636 lgsneg 16028 umgredgnlp 16278 umgr2edg1 16335 umgr2edgneu 16338 |
| Copyright terms: Public domain | W3C validator |