![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impbid2 | Unicode version |
Description: Infer an equivalence from two implications. (Contributed by NM, 6-Mar-2007.) (Proof shortened by Wolf Lammen, 27-Sep-2013.) |
Ref | Expression |
---|---|
impbid2.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
impbid2.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
impbid2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbid2.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | impbid2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 1, 2 | impbid1 141 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomd 140 |
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-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: biimt 240 mtt 651 biorf 704 biorfi 706 pm4.72 778 biort 780 imanst 785 con34bdc 809 notnotbdc 810 dfandc 822 dfordc 835 dfor2dc 838 pm4.79dc 853 orimdidc 856 pm5.54dc 871 pm5.62dc 897 bimsc1 915 modc 2003 euan 2016 exmoeudc 2023 nebidc 2347 cgsexg 2676 cgsex2g 2677 cgsex4g 2678 elab3gf 2787 abidnf 2805 elsn2g 3505 difsn 3604 prel12 3645 dfnfc2 3701 intmin4 3746 dfiin2g 3793 elpw2g 4021 ordsucg 4356 ssrel 4565 ssrel2 4567 ssrelrel 4577 releldmb 4714 relelrnb 4715 cnveqb 4930 dmsnopg 4946 relcnvtr 4994 relcnvexb 5014 f1ocnvb 5315 ffvresb 5515 fconstfvm 5570 fnoprabg 5804 dfsmo2 6114 nntri2 6320 nntri1 6322 en1bg 6624 djulclb 6855 nngt1ne1 8613 znegclb 8939 iccneg 9613 fzsn 9687 fz1sbc 9717 fzofzp1b 9846 ceilqidz 9930 flqeqceilz 9932 reim0b 10475 rexanre 10832 dvdsext 11348 zob 11383 eltg3 12008 bastop 12026 cnptoprest 12189 bj-om 12720 |
Copyright terms: Public domain | W3C validator |