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 130 | . 2 ⊢ (𝜑 → (𝜒 ↔ 𝜓)) |
4 | 3 | bicomd 129 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: biimt 230 mtt 610 biorf 663 biorfi 665 pm4.72 736 biort 738 con34bdc 765 notnotbdc 766 dfandc 778 dfordc 791 dfor2dc 794 pm4.79dc 809 orimdidc 812 pm5.54dc 827 pm5.62dc 852 bimsc1 870 modc 1943 euan 1956 exmoeudc 1963 nebidc 2285 cgsexg 2589 cgsex2g 2590 cgsex4g 2591 elab3gf 2692 abidnf 2709 elsn2g 3404 difsn 3501 prel12 3542 dfnfc2 3598 intmin4 3643 dfiin2g 3690 elpw2g 3910 ordsucg 4228 ssrel 4428 ssrel2 4430 ssrelrel 4440 releldmb 4571 relelrnb 4572 cnveqb 4776 dmsnopg 4792 relcnvtr 4840 relcnvexb 4857 f1ocnvb 5140 ffvresb 5328 fconstfvm 5379 fnoprabg 5602 dfsmo2 5902 nntri2 6073 nntri1 6074 en1bg 6280 nngt1ne1 7948 znegclb 8278 iccneg 8857 fzsn 8929 fz1sbc 8958 fzofzp1b 9084 ceilqidz 9158 flqeqceilz 9160 reim0b 9462 bj-om 10061 |
Copyright terms: Public domain | W3C validator |