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 141 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
4 | 3 | bicomd 140 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 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 675 biorf 734 biorfi 736 pm4.72 813 con34bdc 857 notnotbdc 858 dfandc 870 imanst 874 dfordc 878 dfor2dc 881 pm4.79dc 889 orimdidc 892 pm5.54dc 904 pm5.62dc 930 bimsc1 948 modc 2049 euan 2062 exmoeudc 2069 nebidc 2407 cgsexg 2747 cgsex2g 2748 cgsex4g 2749 elab3gf 2862 abidnf 2880 elsn2g 3594 difsn 3695 prel12 3736 dfnfc2 3792 intmin4 3837 dfiin2g 3884 elpw2g 4120 ordsucg 4464 ssrel 4677 ssrel2 4679 ssrelrel 4689 releldmb 4826 relelrnb 4827 cnveqb 5044 dmsnopg 5060 relcnvtr 5108 relcnvexb 5128 f1ocnvb 5431 ffvresb 5633 fconstfvm 5688 fnoprabg 5925 dfsmo2 6237 nntri2 6444 nntri1 6446 en1bg 6748 fieq0 6923 djulclb 7002 ismkvnex 7101 nngt1ne1 8874 znegclb 9206 iccneg 9900 fzsn 9975 fz1sbc 10005 fzofzp1b 10137 ceilqidz 10225 flqeqceilz 10227 reim0b 10774 rexanre 11132 dvdsext 11760 zob 11795 eltg3 12553 bastop 12571 cnptoprest 12735 cos11 13270 bj-om 13609 |
Copyright terms: Public domain | W3C validator |