![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp1d | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simp1d |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp1 946 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
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 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: simp1bi 961 erinxp 6406 addcanprleml 7270 addcanprlemu 7271 ltmprr 7298 lelttrdi 8001 ixxdisj 9469 ixxss1 9470 ixxss2 9471 ixxss12 9472 iccss2 9510 iocssre 9519 icossre 9520 iccssre 9521 icodisj 9558 iccf1o 9570 fzen 9606 ioom 9821 intfracq 9876 flqdiv 9877 mulqaddmodid 9920 modsumfzodifsn 9952 addmodlteq 9954 remul 10437 sumtp 10973 crth 11643 phimullem 11644 strsetsid 11692 strleund 11747 lmfpm 12110 lmff 12116 lmtopcnp 12117 xmeter 12238 tgqioo 12337 |
Copyright terms: Public domain | W3C validator |