| 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 1023 |
. 2
| |
| 3 | 1, 2 | syl 14 |
1
|
| Colors of variables: wff set class |
| Syntax hints: |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 |
| This theorem depends on definitions: df-bi 117 df-3an 1006 |
| This theorem is referenced by: simp1bi 1038 erinxp 6778 exmidapne 7479 addcanprleml 7834 addcanprlemu 7835 ltmprr 7862 lelttrdi 8606 ixxdisj 10138 ixxss1 10139 ixxss2 10140 ixxss12 10141 iccss2 10179 iocssre 10188 icossre 10189 iccssre 10190 icodisj 10227 iccf1o 10239 fzen 10278 ioom 10521 intfracq 10583 flqdiv 10584 mulqaddmodid 10627 modsumfzodifsn 10659 addmodlteq 10661 remul 11437 sumtp 11980 crth 12801 phimullem 12802 eulerthlem1 12804 eulerthlemfi 12805 eulerthlemrprm 12806 eulerthlema 12807 eulerthlemh 12808 eulerthlemth 12809 ctiunct 13066 strsetsid 13120 strleund 13191 strext 13193 mhmf 13553 submss 13564 eqger 13816 eqgcpbl 13820 lmodvscl 14325 lssssg 14380 rnglidlmsgrp 14517 2idlcpblrng 14543 lmfpm 14973 lmff 14979 lmtopcnp 14980 xmeter 15166 tgqioo 15285 ivthinclemlopn 15366 ivthinclemuopn 15368 limcimolemlt 15394 limcresi 15396 cosordlem 15579 relogbval 15681 relogbzcl 15682 nnlogbexp 15689 perfectlem2 15730 wlkprop 16184 wlkf 16187 wlkfg 16188 wlkvtxiedg 16202 wlk1walkdom 16216 wlkvtxedg 16220 upgr2wlkdc 16234 isclwwlkng 16263 eupthseg 16309 trlsegvdeglem3 16319 trlsegvdeglem5 16321 depindlem2 16352 depindlem3 16353 |
| Copyright terms: Public domain | W3C validator |