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 987 | . 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 |
This theorem depends on definitions: df-bi 116 df-3an 969 |
This theorem is referenced by: simp2bi 1002 erinxp 6566 resixp 6690 addcanprleml 7546 addcanprlemu 7547 ltmprr 7574 lelttrdi 8315 ixxdisj 9830 ixxss1 9831 ixxss2 9832 ixxss12 9833 iccgelb 9859 iccss2 9871 icodisj 9919 ioom 10186 elicore 10192 flqdiv 10246 mulqaddmodid 10289 modsumfzodifsn 10321 addmodlteq 10323 immul 10807 sumtp 11341 crth 12135 phimullem 12136 eulerthlem1 12138 eulerthlema 12141 eulerthlemh 12142 eulerthlemth 12143 ctiunct 12316 structn0fun 12350 strleund 12425 lmcl 12792 lmtopcnp 12797 xmeter 12983 tgqioo 13094 ivthinclemlopn 13161 ivthinclemuopn 13163 limcimolemlt 13180 limcresi 13182 limccnpcntop 13191 limccnp2lem 13192 limccnp2cntop 13193 cosordlem 13317 |
Copyright terms: Public domain | W3C validator |