![]() |
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 950 |
. 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 932 |
This theorem is referenced by: simp2bi 965 erinxp 6433 resixp 6557 addcanprleml 7323 addcanprlemu 7324 ltmprr 7351 lelttrdi 8055 ixxdisj 9527 ixxss1 9528 ixxss2 9529 ixxss12 9530 iccgelb 9556 iccss2 9568 icodisj 9616 ioom 9879 flqdiv 9935 mulqaddmodid 9978 modsumfzodifsn 10010 addmodlteq 10012 immul 10492 sumtp 11022 crth 11692 phimullem 11693 structn0fun 11754 strleund 11829 lmcl 12195 lmtopcnp 12200 xmeter 12364 tgqioo 12466 limcimolemlt 12513 limcresi 12515 limccnpcntop 12520 |
Copyright terms: Public domain | W3C validator |