| 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 11450 sumtp 11993 crth 12814 phimullem 12815 eulerthlem1 12817 eulerthlemfi 12818 eulerthlemrprm 12819 eulerthlema 12820 eulerthlemh 12821 eulerthlemth 12822 ctiunct 13079 strsetsid 13133 strleund 13204 strext 13206 mhmf 13566 submss 13577 eqger 13829 eqgcpbl 13833 lmodvscl 14338 lssssg 14393 rnglidlmsgrp 14530 2idlcpblrng 14556 lmfpm 14986 lmff 14992 lmtopcnp 14993 xmeter 15179 tgqioo 15298 ivthinclemlopn 15379 ivthinclemuopn 15381 limcimolemlt 15407 limcresi 15409 cosordlem 15592 relogbval 15694 relogbzcl 15695 nnlogbexp 15702 perfectlem2 15743 wlkprop 16197 wlkf 16200 wlkfg 16201 wlkvtxiedg 16215 wlk1walkdom 16229 wlkvtxedg 16233 upgr2wlkdc 16247 isclwwlkng 16276 eupthseg 16322 trlsegvdeglem3 16332 trlsegvdeglem5 16334 depindlem2 16377 depindlem3 16378 |
| Copyright terms: Public domain | W3C validator |