![]() |
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-1 5 ax-2 6 ax-mp 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 646 biorf 699 biorfi 701 pm4.72 773 biort 775 imanst 780 con34bdc 804 notnotbdc 805 dfandc 817 dfordc 830 dfor2dc 833 pm4.79dc 848 orimdidc 851 pm5.54dc 866 pm5.62dc 892 bimsc1 910 modc 1992 euan 2005 exmoeudc 2012 nebidc 2336 cgsexg 2655 cgsex2g 2656 cgsex4g 2657 elab3gf 2766 abidnf 2784 elsn2g 3481 difsn 3580 prel12 3621 dfnfc2 3677 intmin4 3722 dfiin2g 3769 elpw2g 3998 ordsucg 4332 ssrel 4539 ssrel2 4541 ssrelrel 4551 releldmb 4685 relelrnb 4686 cnveqb 4899 dmsnopg 4915 relcnvtr 4963 relcnvexb 4983 f1ocnvb 5280 ffvresb 5475 fconstfvm 5529 fnoprabg 5760 dfsmo2 6066 nntri2 6269 nntri1 6271 en1bg 6571 djulclb 6801 nngt1ne1 8518 znegclb 8844 iccneg 9467 fzsn 9541 fz1sbc 9571 fzofzp1b 9700 ceilqidz 9784 flqeqceilz 9786 reim0b 10357 rexanre 10714 dvdsext 11195 zob 11230 eltg3 11818 bastop 11836 bj-om 12105 |
Copyright terms: Public domain | W3C validator |