![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impbida | Unicode version |
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.) |
Ref | Expression |
---|---|
impbida.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
impbida.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
impbida |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbida.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | impbida.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 114 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | impbid 128 |
1
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff set class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eqrdav 2139 funfvbrb 5541 f1ocnv2d 5982 1stconst 6126 2ndconst 6127 cnvf1o 6130 ersymb 6451 swoer 6465 erth 6481 enen1 6742 enen2 6743 domen1 6744 domen2 6745 xpmapenlem 6751 fidifsnen 6772 fundmfibi 6835 f1dmvrnfibi 6840 ordiso2 6928 omniwomnimkv 7049 enwomnilem 7050 fzsplit2 9861 fseq1p1m1 9905 elfz2nn0 9923 btwnzge0 10104 modqsubdir 10197 zesq 10441 hashprg 10586 rereb 10667 abslt 10892 absle 10893 maxleastb 11018 maxltsup 11022 xrltmaxsup 11058 xrmaxltsup 11059 iserex 11140 mptfzshft 11243 fsumrev 11244 dvdsadd2b 11576 nn0ob 11641 dfgcd3 11734 dfgcd2 11738 dvdsmulgcd 11749 lcmgcdeq 11800 qden1elz 11919 cncnp 12438 xmetxpbl 12716 dedekindicc 12819 coseq0q4123 12963 coseq0negpitopi 12965 relogeftb 12994 relogbcxpbap 13090 pwf1oexmid 13367 isomninnlem 13400 apdiff 13416 iswomninnlem 13417 ismkvnnlem 13419 redcwlpolemeq1 13421 |
Copyright terms: Public domain | W3C validator |