![]() |
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 999 |
. 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 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 df-3an 980 |
This theorem is referenced by: simp3bi 1014 erinxp 6612 resixp 6736 exmidapne 7262 addcanprleml 7616 addcanprlemu 7617 ltmprr 7644 lelttrdi 8386 ixxdisj 9906 ixxss1 9907 ixxss2 9908 ixxss12 9909 iccsupr 9969 icodisj 9995 ioom 10264 elicore 10270 intfracq 10323 flqdiv 10324 mulqaddmodid 10367 modsumfzodifsn 10399 cjmul 10897 sumtp 11425 crth 12227 eulerthlem1 12230 eulerthlemh 12234 eulerthlemth 12235 ennnfonelemim 12428 ctiunct 12444 strsetsid 12498 strleund 12565 strext 12567 mhm0 12865 submcl 12876 eqger 13089 eqgcpbl 13093 lmodvsdir 13408 lssclg 13457 lmcvg 13857 lmff 13889 lmtopcnp 13890 xmeter 14076 xmetresbl 14080 tgqioo 14187 ivthinclemlopn 14254 ivthinclemuopn 14256 limccl 14268 limcdifap 14271 limcresi 14275 limccnpcntop 14284 limccnp2lem 14285 limccnp2cntop 14286 limccoap 14287 cosordlem 14410 relogbval 14509 relogbzcl 14510 nnlogbexp 14517 |
Copyright terms: Public domain | W3C validator |