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 659 pm3.44 704 orbi2i 751 pm2.31 757 dcor 919 rnlem 960 syl3an1br 1255 syl3an2br 1256 syl3an3br 1257 xorbin 1362 3impexpbicom 1414 equveli 1732 sbbii 1738 dveeq2or 1788 exmoeudc 2062 eueq2dc 2857 ralun 3258 undif3ss 3337 ssunieq 3769 a9evsep 4050 dcextest 4495 tfi 4496 peano5 4512 opelxpi 4571 ndmima 4916 iotass 5105 dffo2 5349 dff1o2 5372 resdif 5389 f1o00 5402 ressnop0 5601 fsnunfv 5621 ovid 5887 ovidig 5888 f1stres 6057 f2ndres 6058 rdgon 6283 elixpsn 6629 diffisn 6787 diffifi 6788 unsnfi 6807 snexxph 6838 ordiso2 6920 omp1eomlem 6979 ltexnqq 7216 enq0sym 7240 prarloclem5 7308 nqprloc 7353 nqprl 7359 nqpru 7360 pitonn 7656 axcnre 7689 peano5nnnn 7700 axcaucvglemres 7707 le2tri3i 7872 muldivdirap 8467 peano5nni 8723 0nn0 8992 uzind4 9383 elfz4 9799 eluzfz 9801 ssfzo12bi 10002 ioom 10038 ser0 10287 exp3vallem 10294 hashinfuni 10523 hashxp 10572 nn0abscl 10857 fimaxre2 10998 iserle 11111 climserle 11114 summodclem2a 11150 fsumcl2lem 11167 fsumadd 11175 sumsnf 11178 isumclim3 11192 isumadd 11200 sumsplitdc 11201 fsummulc2 11217 cvgcmpub 11245 isumshft 11259 isumlessdc 11265 trireciplem 11269 geolim 11280 geo2lim 11285 cvgratz 11301 mertenslem2 11305 mertensabs 11306 prodmodclem3 11344 prodmodclem2a 11345 ef0lem 11366 efcvgfsum 11373 ege2le3 11377 efcj 11379 efgt1p2 11401 ndvdsadd 11628 gcdsupex 11646 gcdsupcl 11647 ialgrlemconst 11724 divgcdcoprmex 11783 1idssfct 11796 tgcl 12233 txcnp 12440 bj-sucexg 13120 bj-indind 13130 bj-2inf 13136 findset 13143 trilpolemisumle 13231 |
Copyright terms: Public domain | W3C validator |