![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > simp2d | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
simp2d |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | simp2 947 |
. 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 ax-ia2 106 |
This theorem depends on definitions: df-bi 116 df-3an 929 |
This theorem is referenced by: simp2bi 962 erinxp 6406 resixp 6530 addcanprleml 7270 addcanprlemu 7271 ltmprr 7298 lelttrdi 8001 ixxdisj 9469 ixxss1 9470 ixxss2 9471 ixxss12 9472 iccgelb 9498 iccss2 9510 icodisj 9558 ioom 9821 flqdiv 9877 mulqaddmodid 9920 modsumfzodifsn 9952 addmodlteq 9954 immul 10444 sumtp 10973 crth 11643 phimullem 11644 structn0fun 11672 strleund 11747 lmcl 12112 lmtopcnp 12117 xmeter 12238 tgqioo 12337 |
Copyright terms: Public domain | W3C validator |