![]() |
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 142 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | 3 | bicomd 141 |
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-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: biimt 241 mtt 686 biorf 745 biorfi 747 pm4.72 828 con34bdc 872 notnotbdc 873 dfandc 885 imanst 889 dfordc 893 dfor2dc 896 pm4.79dc 904 orimdidc 907 pm5.54dc 919 pm5.62dc 946 bimsc1 964 modc 2080 euan 2093 exmoeudc 2100 nebidc 2439 cgsexg 2786 cgsex2g 2787 cgsex4g 2788 elab3gf 2901 abidnf 2919 elsn2g 3639 difsn 3743 prel12 3785 dfnfc2 3841 intmin4 3886 dfiin2g 3933 elpw2g 4170 ordsucg 4515 ssrel 4728 ssrel2 4730 ssrelrel 4740 releldmb 4878 relelrnb 4879 cnveqb 5098 dmsnopg 5114 relcnvtr 5162 relcnvexb 5182 f1ocnvb 5489 ffvresb 5694 fconstfvm 5749 fnoprabg 5991 dfsmo2 6305 nntri2 6512 nntri1 6514 en1bg 6817 fieq0 6992 djulclb 7071 ismkvnex 7170 nngt1ne1 8971 znegclb 9303 iccneg 10006 fzsn 10083 fz1sbc 10113 fzofzp1b 10245 ceilqidz 10333 flqeqceilz 10335 reim0b 10888 rexanre 11246 dvdsext 11878 zob 11913 pc11 12347 pcz 12348 issubg2m 13093 issubg4m 13097 ghmmhmb 13153 opprrngbg 13388 opprringbg 13390 issubrng2 13517 issubrg2 13548 eltg3 13940 bastop 13958 cnptoprest 14122 cos11 14657 zabsle1 14783 lgsabs1 14823 bj-om 15072 |
Copyright terms: Public domain | W3C validator |