![]() |
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 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 594 pm3.44 634 orbi2i 678 pm2.31 684 dcor 842 rnlem 882 syl3an1br 1173 syl3an2br 1174 syl3an3br 1175 xorbin 1272 3impexpbicom 1324 equveli 1639 sbbii 1645 dveeq2or 1694 exmoeudc 1960 eueq2dc 2708 ralun 3119 undif3ss 3192 ssunieq 3604 a9evsep 3870 tfi 4248 peano5 4264 opelxpi 4319 ndmima 4645 iotass 4827 dffo2 5053 dff1o2 5074 resdif 5091 f1o00 5104 ressnop0 5287 fsnunfv 5306 ovid 5559 ovidig 5560 f1stres 5728 f2ndres 5729 ltexnqq 6391 enq0sym 6415 prarloclem5 6483 nqprloc 6528 nqprl 6533 pitonn 6744 axcnre 6765 le2tri3i 6923 peano5nni 7698 0nn0 7972 uzind4 8307 elfz4 8653 eluzfz 8655 ssfzo12bi 8851 nn0abscl 9229 bj-sucexg 9377 bj-indind 9391 bj-2inf 9397 peano5setOLD 9400 findset 9405 |
Copyright terms: Public domain | W3C validator |