Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simp3d | Unicode version |
Description: Deduce a conjunct from a triple conjunction. (Contributed by NM, 4-Sep-2005.) |
Ref | Expression |
---|---|
3simp1d.1 |
Ref | Expression |
---|---|
simp3d |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simp1d.1 | . 2 | |
2 | simp3 988 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 967 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: simp3bi 1003 erinxp 6566 resixp 6690 addcanprleml 7546 addcanprlemu 7547 ltmprr 7574 lelttrdi 8315 ixxdisj 9830 ixxss1 9831 ixxss2 9832 ixxss12 9833 iccsupr 9893 icodisj 9919 ioom 10186 elicore 10192 intfracq 10245 flqdiv 10246 mulqaddmodid 10289 modsumfzodifsn 10321 cjmul 10813 sumtp 11341 crth 12135 eulerthlem1 12138 eulerthlemh 12142 eulerthlemth 12143 ennnfonelemim 12300 ctiunct 12316 strsetsid 12370 strleund 12425 lmcvg 12764 lmff 12796 lmtopcnp 12797 xmeter 12983 xmetresbl 12987 tgqioo 13094 ivthinclemlopn 13161 ivthinclemuopn 13163 limccl 13175 limcdifap 13178 limcresi 13182 limccnpcntop 13191 limccnp2lem 13192 limccnp2cntop 13193 limccoap 13194 cosordlem 13317 relogbval 13416 relogbzcl 13417 nnlogbexp 13424 |
Copyright terms: Public domain | W3C validator |