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 2136 funfvbrb 5526 f1ocnv2d 5967 1stconst 6111 2ndconst 6112 cnvf1o 6115 ersymb 6436 swoer 6450 erth 6466 enen1 6727 enen2 6728 domen1 6729 domen2 6730 xpmapenlem 6736 fidifsnen 6757 fundmfibi 6820 f1dmvrnfibi 6825 ordiso2 6913 fzsplit2 9823 fseq1p1m1 9867 elfz2nn0 9885 btwnzge0 10066 modqsubdir 10159 zesq 10403 hashprg 10547 rereb 10628 abslt 10853 absle 10854 maxleastb 10979 maxltsup 10983 xrltmaxsup 11019 xrmaxltsup 11020 iserex 11101 mptfzshft 11204 fsumrev 11205 dvdsadd2b 11529 nn0ob 11594 dfgcd3 11687 dfgcd2 11691 dvdsmulgcd 11702 lcmgcdeq 11753 qden1elz 11872 cncnp 12388 xmetxpbl 12666 dedekindicc 12769 coseq0q4123 12904 coseq0negpitopi 12906 pwf1oexmid 13183 isomninnlem 13214 |
Copyright terms: Public domain | W3C validator |