![]() |
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 609 biorf 662 biorfi 664 pm4.72 735 biort 737 con34bdc 764 notnotdc 765 dfandc 777 dfordc 790 dfor2dc 793 pm4.79dc 808 orimdidc 811 pm5.54dc 826 pm5.62dc 851 bimsc1 869 modc 1940 euan 1953 exmoeudc 1960 nebidc 2279 cgsexg 2583 cgsex2g 2584 cgsex4g 2585 elab3gf 2686 abidnf 2703 elsnc2g 3396 difsn 3492 prel12 3533 dfnfc2 3589 intmin4 3634 dfiin2g 3681 elpw2g 3901 ordsucg 4194 ssrel 4371 ssrel2 4373 ssrelrel 4383 releldmb 4514 relelrnb 4515 cnveqb 4719 dmsnopg 4735 relcnvtr 4783 relcnvexb 4800 f1ocnvb 5083 ffvresb 5271 fconstfvm 5322 fnoprabg 5544 dfsmo2 5843 nntri2 6012 nntri1 6013 en1bg 6216 nngt1ne1 7729 znegclb 8054 iccneg 8627 fzsn 8699 fz1sbc 8728 fzofzp1b 8854 reim0b 9090 bj-om 9396 |
Copyright terms: Public domain | W3C validator |