Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > biimpri | Unicode version |
Description: Infer a converse implication from a logical equivalence. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 16-Sep-2013.) |
Ref | Expression |
---|---|
biimpri.1 |
Ref | Expression |
---|---|
biimpri |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | biimpri.1 | . . 3 | |
2 | 1 | bicomi 131 | . 2 |
3 | 2 | biimpi 119 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: sylibr 133 sylbir 134 sylbbr 135 sylbb1 136 sylbb2 137 mpbir 145 syl5bir 152 syl6ibr 161 bitri 183 sylanbr 283 sylan2br 286 simplbi2 382 sylanblrc 412 mtbi 644 pm3.44 689 orbi2i 736 pm2.31 742 dcor 904 rnlem 945 syl3an1br 1240 syl3an2br 1241 syl3an3br 1242 xorbin 1347 3impexpbicom 1399 equveli 1717 sbbii 1723 dveeq2or 1772 exmoeudc 2040 eueq2dc 2830 ralun 3228 undif3ss 3307 ssunieq 3739 a9evsep 4020 dcextest 4465 tfi 4466 peano5 4482 opelxpi 4541 ndmima 4886 iotass 5075 dffo2 5319 dff1o2 5340 resdif 5357 f1o00 5370 ressnop0 5569 fsnunfv 5589 ovid 5855 ovidig 5856 f1stres 6025 f2ndres 6026 rdgon 6251 elixpsn 6597 diffisn 6755 diffifi 6756 unsnfi 6775 snexxph 6806 ordiso2 6888 omp1eomlem 6947 ltexnqq 7184 enq0sym 7208 prarloclem5 7276 nqprloc 7321 nqprl 7327 nqpru 7328 pitonn 7624 axcnre 7657 peano5nnnn 7668 axcaucvglemres 7675 le2tri3i 7840 muldivdirap 8435 peano5nni 8691 0nn0 8960 uzind4 9351 elfz4 9767 eluzfz 9769 ssfzo12bi 9970 ioom 10006 ser0 10255 exp3vallem 10262 hashinfuni 10491 hashxp 10540 nn0abscl 10825 fimaxre2 10966 iserle 11079 climserle 11082 summodclem2a 11118 fsumcl2lem 11135 fsumadd 11143 sumsnf 11146 isumclim3 11160 isumadd 11168 sumsplitdc 11169 fsummulc2 11185 cvgcmpub 11213 isumshft 11227 isumlessdc 11233 trireciplem 11237 geolim 11248 geo2lim 11253 cvgratz 11269 mertenslem2 11273 mertensabs 11274 ef0lem 11293 efcvgfsum 11300 ege2le3 11304 efcj 11306 efgt1p2 11328 ndvdsadd 11555 gcdsupex 11573 gcdsupcl 11574 ialgrlemconst 11651 divgcdcoprmex 11710 1idssfct 11723 tgcl 12160 txcnp 12367 bj-sucexg 13047 bj-indind 13057 bj-2inf 13063 findset 13070 trilpolemisumle 13158 |
Copyright terms: Public domain | W3C validator |