![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > biimpri | GIF 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 130 | . 2 ⊢ (𝜓 ↔ 𝜑) |
3 | 2 | biimpi 118 | 1 ⊢ (𝜓 → 𝜑) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 103 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 104 ax-ia2 105 ax-ia3 106 |
This theorem depends on definitions: df-bi 115 |
This theorem is referenced by: sylibr 132 sylbir 133 sylbbr 134 sylbb1 135 sylbb2 136 mpbir 144 syl5bir 151 syl6ibr 160 bitri 182 sylanbr 279 sylan2br 282 simplbi2 377 sylanblrc 407 mtbi 628 pm3.44 668 orbi2i 712 pm2.31 718 dcor 879 rnlem 920 syl3an1br 1211 syl3an2br 1212 syl3an3br 1213 xorbin 1318 3impexpbicom 1370 equveli 1686 sbbii 1692 dveeq2or 1741 exmoeudc 2008 eueq2dc 2778 ralun 3168 undif3ss 3246 ssunieq 3663 a9evsep 3929 dcextest 4362 tfi 4363 peano5 4379 opelxpi 4435 ndmima 4767 iotass 4954 dffo2 5188 dff1o2 5209 resdif 5226 f1o00 5239 ressnop0 5423 fsnunfv 5442 ovid 5699 ovidig 5700 f1stres 5868 f2ndres 5869 rdgon 6086 diffisn 6542 diffifi 6543 unsnfi 6559 snexxph 6586 ordiso2 6649 ltexnqq 6888 enq0sym 6912 prarloclem5 6980 nqprloc 7025 nqprl 7031 nqpru 7032 pitonn 7306 axcnre 7337 peano5nnnn 7348 axcaucvglemres 7355 le2tri3i 7514 muldivdirap 8090 peano5nni 8337 0nn0 8598 uzind4 8985 elfz4 9342 eluzfz 9344 ssfzo12bi 9539 ioom 9575 iser0 9801 hashinfuni 10034 hashxp 10083 nn0abscl 10359 fimaxre2 10497 iserile 10568 ndvdsadd 10725 gcdsupex 10743 gcdsupcl 10744 ialgrlemconst 10819 divgcdcoprmex 10878 1idssfct 10891 bj-sucexg 11170 bj-indind 11184 bj-2inf 11190 findset 11197 |
Copyright terms: Public domain | W3C validator |