![]() |
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 966 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | syl 14 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 df-3an 947 |
This theorem is referenced by: simp3bi 981 erinxp 6457 resixp 6581 addcanprleml 7370 addcanprlemu 7371 ltmprr 7398 lelttrdi 8107 ixxdisj 9579 ixxss1 9580 ixxss2 9581 ixxss12 9582 iccsupr 9642 icodisj 9668 ioom 9931 intfracq 9986 flqdiv 9987 mulqaddmodid 10030 modsumfzodifsn 10062 cjmul 10550 sumtp 11075 crth 11745 ennnfonelemim 11782 ctiunct 11796 strsetsid 11835 strleund 11890 lmcvg 12228 lmff 12260 lmtopcnp 12261 xmeter 12425 xmetresbl 12429 tgqioo 12533 limccl 12584 limcdifap 12587 limcresi 12591 limccnpcntop 12600 limccnp2lem 12601 limccnp2cntop 12602 |
Copyright terms: Public domain | W3C validator |