Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > impbida | GIF version |
Description: Deduce an equivalence from two implications. (Contributed by NM, 17-Feb-2007.) |
Ref | Expression |
---|---|
impbida.1 | ⊢ ((𝜑 ∧ 𝜓) → 𝜒) |
impbida.2 | ⊢ ((𝜑 ∧ 𝜒) → 𝜓) |
Ref | Expression |
---|---|
impbida | ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | impbida.1 | . . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒) | |
2 | 1 | ex 114 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | impbida.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | |
4 | 3 | ex 114 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 2, 4 | impbid 128 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 103 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: eqrdav 2156 funfvbrb 5580 f1ocnv2d 6024 1stconst 6168 2ndconst 6169 cnvf1o 6172 ersymb 6494 swoer 6508 erth 6524 enen1 6785 enen2 6786 domen1 6787 domen2 6788 xpmapenlem 6794 fidifsnen 6815 fundmfibi 6883 f1dmvrnfibi 6888 ordiso2 6979 omniwomnimkv 7110 enwomnilem 7112 infregelbex 9509 fzsplit2 9952 fseq1p1m1 9996 elfz2nn0 10014 btwnzge0 10199 modqsubdir 10292 zesq 10536 hashprg 10682 rereb 10763 abslt 10988 absle 10989 maxleastb 11114 maxltsup 11118 xrltmaxsup 11154 xrmaxltsup 11155 iserex 11236 mptfzshft 11339 fsumrev 11340 fprodrev 11516 dvdsadd2b 11733 nn0ob 11798 dfgcd3 11893 dfgcd2 11897 dvdsmulgcd 11908 lcmgcdeq 11959 qden1elz 12079 cncnp 12630 xmetxpbl 12908 dedekindicc 13011 coseq0q4123 13155 coseq0negpitopi 13157 relogeftb 13186 relogbcxpbap 13282 pwf1oexmid 13571 isomninnlem 13601 apdiff 13619 iswomninnlem 13620 ismkvnnlem 13623 redcwlpolemeq1 13625 |
Copyright terms: Public domain | W3C validator |