Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl2 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl2 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp2 905 | . 2 | |
2 | 1 | adantr 261 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wa 97 w3a 885 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: simpll2 944 simprl2 950 simp1l2 998 simp2l2 1004 simp3l2 1010 3anandirs 1238 rspc3ev 2666 tfisi 4310 brcogw 4504 oawordi 6049 nnmord 6090 nnmword 6091 ac6sfi 6352 ordiso2 6357 prarloclemarch2 6517 enq0tr 6532 distrlem4prl 6682 distrlem4pru 6683 ltaprg 6717 aptiprlemu 6738 lelttr 7106 ltletr 7107 readdcan 7153 addcan 7191 addcan2 7192 ltadd2 7416 ltmul1a 7582 ltmul1 7583 lemul1a 7824 xrlelttr 8722 xrltletr 8723 ixxdisj 8772 icoshftf1o 8859 icodisj 8860 lincmb01cmp 8871 iccf1o 8872 fztri3or 8903 ltexp2a 9306 exple1 9310 expnbnd 9372 expnlbnd2 9374 addcn2 9831 mulcn2 9833 |
Copyright terms: Public domain | W3C validator |