![]() |
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 998 |
. 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 981 |
This theorem is referenced by: simp1bi 1013 erinxp 6622 exmidapne 7272 addcanprleml 7626 addcanprlemu 7627 ltmprr 7654 lelttrdi 8396 ixxdisj 9916 ixxss1 9917 ixxss2 9918 ixxss12 9919 iccss2 9957 iocssre 9966 icossre 9967 iccssre 9968 icodisj 10005 iccf1o 10017 fzen 10056 ioom 10274 intfracq 10333 flqdiv 10334 mulqaddmodid 10377 modsumfzodifsn 10409 addmodlteq 10411 remul 10894 sumtp 11435 crth 12237 phimullem 12238 eulerthlem1 12240 eulerthlemfi 12241 eulerthlemrprm 12242 eulerthlema 12243 eulerthlemh 12244 eulerthlemth 12245 ctiunct 12454 strsetsid 12508 strleund 12576 strext 12578 mhmf 12877 submss 12888 eqger 13115 eqgcpbl 13119 lmodvscl 13489 lssssg 13544 lmfpm 14014 lmff 14020 lmtopcnp 14021 xmeter 14207 tgqioo 14318 ivthinclemlopn 14385 ivthinclemuopn 14387 limcimolemlt 14404 limcresi 14406 cosordlem 14541 relogbval 14640 relogbzcl 14641 nnlogbexp 14648 |
Copyright terms: Public domain | W3C validator |