![]() |
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 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | impbida.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 115 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | impbid 129 |
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 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biadanid 614 eqrdav 2186 funfvbrb 5642 f1ocnv2d 6089 1stconst 6236 2ndconst 6237 cnvf1o 6240 ersymb 6563 swoer 6577 erth 6593 enen1 6854 enen2 6855 domen1 6856 domen2 6857 xpmapenlem 6863 fidifsnen 6884 fundmfibi 6952 f1dmvrnfibi 6957 ordiso2 7048 omniwomnimkv 7179 enwomnilem 7181 nninfwlpoimlemginf 7188 exmidapne 7273 infregelbex 9612 fzsplit2 10064 fseq1p1m1 10108 elfz2nn0 10126 btwnzge0 10314 modqsubdir 10407 zesq 10653 hashprg 10802 rereb 10886 abslt 11111 absle 11112 maxleastb 11237 maxltsup 11241 xrltmaxsup 11279 xrmaxltsup 11280 iserex 11361 mptfzshft 11464 fsumrev 11465 fprodrev 11641 dvdsadd2b 11861 nn0ob 11927 dfgcd3 12025 dfgcd2 12029 dvdsmulgcd 12040 lcmgcdeq 12097 isprm5 12156 qden1elz 12219 issubmnd 12865 mhmf1o 12883 subsubm 12896 resmhm2b 12902 grpinvid1 12957 grpinvid2 12958 subsubg 13097 ssnmz 13111 ghmf1 13167 kerf1ghm 13168 ghmf1o 13169 conjnmzb 13174 0unit 13434 subsubrng 13491 subrgunit 13516 subsubrg 13522 islss3 13625 islss4 13628 lspsnel6 13654 lspsneq0b 13673 dflidl2rng 13727 cncnp 14083 xmetxpbl 14361 dedekindicc 14464 coseq0q4123 14608 coseq0negpitopi 14610 relogeftb 14639 relogbcxpbap 14736 pwf1oexmid 15103 isomninnlem 15132 apdiff 15150 iswomninnlem 15151 ismkvnnlem 15154 redcwlpolemeq1 15156 |
Copyright terms: Public domain | W3C validator |