![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > imnan | Unicode version |
Description: Express implication in terms of conjunction. (Contributed by NM, 9-Apr-1994.) (Revised by Mario Carneiro, 1-Feb-2015.) |
Ref | Expression |
---|---|
imnan |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm3.2im 602 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | imp 123 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | con2i 593 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | pm3.2 138 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | con3rr3 599 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | 3, 5 | impbii 125 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 ax-in1 580 ax-in2 581 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: imnani 661 nan 662 pm3.24 663 imanst 780 imandc 825 ianordc 838 pm5.17dc 849 dn1dc 907 xorbin 1321 xordc1 1330 alinexa 1540 dfrex2dc 2372 ralinexa 2406 rabeq0 3318 disj 3337 minel 3350 disjsn 3510 sotricim 4161 poirr2 4839 funun 5073 imadiflem 5108 imadif 5109 brprcneu 5313 prltlu 7109 caucvgprlemnbj 7289 caucvgprprlemnbj 7315 xrltnsym2 9327 fzp1nel 9581 fsumsplit 10864 sumsplitdc 10889 phiprmpw 11539 |
Copyright terms: Public domain | W3C validator |