![]() |
Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > ILE Home > Th. List > impbid2 | GIF 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: → wi 4 ↔ wb 105 |
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 2079 euan 2092 exmoeudc 2099 nebidc 2437 cgsexg 2784 cgsex2g 2785 cgsex4g 2786 elab3gf 2899 abidnf 2917 elsn2g 3637 difsn 3741 prel12 3783 dfnfc2 3839 intmin4 3884 dfiin2g 3931 elpw2g 4168 ordsucg 4513 ssrel 4726 ssrel2 4728 ssrelrel 4738 releldmb 4876 relelrnb 4877 cnveqb 5096 dmsnopg 5112 relcnvtr 5160 relcnvexb 5180 f1ocnvb 5487 ffvresb 5692 fconstfvm 5747 fnoprabg 5989 dfsmo2 6302 nntri2 6509 nntri1 6511 en1bg 6814 fieq0 6989 djulclb 7068 ismkvnex 7167 nngt1ne1 8968 znegclb 9300 iccneg 10003 fzsn 10080 fz1sbc 10110 fzofzp1b 10242 ceilqidz 10330 flqeqceilz 10332 reim0b 10885 rexanre 11243 dvdsext 11875 zob 11910 pc11 12344 pcz 12345 issubg2m 13081 issubg4m 13085 opprrngbg 13326 opprringbg 13328 issubrng2 13430 issubrg2 13461 eltg3 13853 bastop 13871 cnptoprest 14035 cos11 14570 zabsle1 14696 lgsabs1 14736 bj-om 14985 |
Copyright terms: Public domain | W3C validator |