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 992 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 973 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 |
This theorem depends on definitions: df-bi 116 df-3an 975 |
This theorem is referenced by: simp1bi 1007 erinxp 6583 addcanprleml 7563 addcanprlemu 7564 ltmprr 7591 lelttrdi 8332 ixxdisj 9847 ixxss1 9848 ixxss2 9849 ixxss12 9850 iccss2 9888 iocssre 9897 icossre 9898 iccssre 9899 icodisj 9936 iccf1o 9948 fzen 9986 ioom 10204 intfracq 10263 flqdiv 10264 mulqaddmodid 10307 modsumfzodifsn 10339 addmodlteq 10341 remul 10823 sumtp 11364 crth 12165 phimullem 12166 eulerthlem1 12168 eulerthlemfi 12169 eulerthlemrprm 12170 eulerthlema 12171 eulerthlemh 12172 eulerthlemth 12173 ctiunct 12382 strsetsid 12436 strleund 12493 mhmf 12675 submss 12685 lmfpm 12996 lmff 13002 lmtopcnp 13003 xmeter 13189 tgqioo 13300 ivthinclemlopn 13367 ivthinclemuopn 13369 limcimolemlt 13386 limcresi 13388 cosordlem 13523 relogbval 13622 relogbzcl 13623 nnlogbexp 13630 |
Copyright terms: Public domain | W3C validator |