![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eqrdav 2094 funfvbrb 5451 f1ocnv2d 5886 1stconst 6024 2ndconst 6025 cnvf1o 6028 ersymb 6346 swoer 6360 erth 6376 enen1 6636 enen2 6637 domen1 6638 domen2 6639 xpmapenlem 6645 fidifsnen 6666 fundmfibi 6728 f1dmvrnfibi 6733 ordiso2 6808 fzsplit2 9613 fseq1p1m1 9657 elfz2nn0 9675 btwnzge0 9856 modqsubdir 9949 zesq 10187 hashprg 10331 rereb 10412 abslt 10636 absle 10637 maxleastb 10762 maxltsup 10766 xrltmaxsup 10800 xrmaxltsup 10801 iserex 10882 mptfzshft 10985 fsumrev 10986 dvdsadd2b 11270 nn0ob 11335 dfgcd3 11426 dfgcd2 11430 dvdsmulgcd 11441 lcmgcdeq 11492 qden1elz 11610 cncnp 12081 |
Copyright terms: Public domain | W3C validator |