![]() |
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 1000 |
. 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 |
This theorem depends on definitions: df-bi 117 df-3an 982 |
This theorem is referenced by: simp2bi 1015 erinxp 6636 resixp 6760 exmidapne 7290 addcanprleml 7644 addcanprlemu 7645 ltmprr 7672 lelttrdi 8414 ixxdisj 9935 ixxss1 9936 ixxss2 9937 ixxss12 9938 iccgelb 9964 iccss2 9976 icodisj 10024 ioom 10293 elicore 10299 flqdiv 10354 mulqaddmodid 10397 modsumfzodifsn 10429 addmodlteq 10431 immul 10923 sumtp 11457 crth 12259 phimullem 12260 eulerthlem1 12262 eulerthlema 12265 eulerthlemh 12266 eulerthlemth 12267 ctiunct 12494 structn0fun 12528 strleund 12618 strext 12620 mhmlin 12934 subm0cl 12945 eqger 13180 eqgcpbl 13184 lmodvsdi 13644 lss0cl 13702 rnglidlmsgrp 13830 2idlcpblrng 13855 lmcl 14222 lmtopcnp 14227 xmeter 14413 tgqioo 14524 ivthinclemlopn 14591 ivthinclemuopn 14593 limcimolemlt 14610 limcresi 14612 limccnpcntop 14621 limccnp2lem 14622 limccnp2cntop 14623 cosordlem 14747 |
Copyright terms: Public domain | W3C validator |