Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl1 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl1 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp1 904 | . 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: simpll1 943 simprl1 949 simp1l1 997 simp2l1 1003 simp3l1 1009 3anandirs 1238 rspc3ev 2666 brcogw 4504 cocan1 5427 oawordi 6049 nnmord 6090 nnmword 6091 dif1en 6337 ac6sfi 6352 ordiso2 6357 enq0tr 6532 distrlem4prl 6682 distrlem4pru 6683 ltaprg 6717 aptiprlemu 6738 lelttr 7106 readdcan 7153 addcan 7191 addcan2 7192 ltadd2 7416 ltmul1a 7582 ltmul1 7583 lemul1a 7824 xrlelttr 8722 icoshftf1o 8859 lincmb01cmp 8871 iccf1o 8872 fztri3or 8903 fzofzim 9044 ltexp2a 9306 exple1 9310 expnlbnd2 9374 addcn2 9831 mulcn2 9833 |
Copyright terms: Public domain | W3C validator |