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 904 | . 2 | |
3 | 1, 2 | syl 14 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: simp1bi 919 erinxp 6180 addcanprleml 6712 addcanprlemu 6713 ltmprr 6740 lelttrdi 7421 ixxdisj 8772 ixxss1 8773 ixxss2 8774 ixxss12 8775 iccss2 8813 iocssre 8822 icossre 8823 iccssre 8824 icodisj 8860 iccf1o 8872 fzen 8907 intfracq 9162 flqdiv 9163 remul 9472 |
Copyright terms: Public domain | W3C validator |