| 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 6441 cauappcvgprlemladdrl 7988 caucvgprlemladdrl 8009 xrrebnd 10174 fzpreddisj 10430 fzp1nel 10463 fprodntrivap 12299 bitsfzo 12670 bitsmod 12671 gcdsupex 12682 gcdsupcl 12683 gcdnncl 12692 gcd2n0cl 12694 qredeu 12823 cncongr2 12830 divnumden 12922 divdenle 12923 phisum 12967 pythagtriplem4 12995 pythagtriplem8 12999 pythagtriplem9 13000 isnsgrp 13673 ivthinclemdisj 15635 lgsneg 16027 umgredgnlp 16277 umgr2edg1 16334 umgr2edgneu 16337 |
| Copyright terms: Public domain | W3C validator |