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 123 | . 2 |
3 | 2 | biimpi 113 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
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 |
This theorem is referenced by: sylbir 125 mpbir 134 sylibr 137 syl5bir 142 syl6ibr 151 bitri 173 sylanbr 269 sylan2br 272 simplbi2 367 mtbi 595 pm3.44 635 orbi2i 679 pm2.31 685 dcor 843 rnlem 883 syl3an1br 1174 syl3an2br 1175 syl3an3br 1176 xorbin 1275 3impexpbicom 1327 equveli 1642 sbbii 1648 dveeq2or 1697 exmoeudc 1963 eueq2dc 2714 ralun 3125 undif3ss 3198 ssunieq 3613 a9evsep 3879 tfi 4305 peano5 4321 opelxpi 4376 ndmima 4702 iotass 4884 dffo2 5110 dff1o2 5131 resdif 5148 f1o00 5161 ressnop0 5344 fsnunfv 5363 ovid 5617 ovidig 5618 f1stres 5786 f2ndres 5787 diffisn 6350 diffifi 6351 ordiso2 6357 ltexnqq 6506 enq0sym 6530 prarloclem5 6598 nqprloc 6643 nqprl 6649 nqpru 6650 pitonn 6924 axcnre 6955 peano5nnnn 6966 axcaucvglemres 6973 le2tri3i 7126 peano5nni 7917 0nn0 8196 uzind4 8531 elfz4 8883 eluzfz 8885 ssfzo12bi 9081 iser0 9250 nn0abscl 9681 iserile 9862 ialgrlemconst 9882 bj-sucexg 10042 bj-indind 10056 bj-2inf 10062 peano5setOLD 10065 findset 10070 |
Copyright terms: Public domain | W3C validator |