Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > simpl3 | Unicode version |
Description: Simplification rule. (Contributed by Jeff Hankins, 17-Nov-2009.) |
Ref | Expression |
---|---|
simpl3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simp3 906 | . 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 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 df-3an 887 |
This theorem is referenced by: simpll3 945 simprl3 951 simp1l3 999 simp2l3 1005 simp3l3 1011 3anandirs 1238 frirrg 4087 fcofo 5424 acexmid 5511 oawordi 6049 nnmord 6090 nnmword 6091 fidifsnen 6331 dif1en 6337 ac6sfi 6352 enq0tr 6532 distrlem4prl 6682 distrlem4pru 6683 ltaprg 6717 lelttr 7106 ltletr 7107 readdcan 7153 addcan 7191 addcan2 7192 ltadd2 7416 xrlelttr 8722 xrltletr 8723 icoshftf1o 8859 difelfzle 8992 fzo1fzo0n0 9039 ltexp2a 9306 exple1 9310 expnlbnd2 9374 addcn2 9831 mulcn2 9833 |
Copyright terms: Public domain | W3C validator |