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 2116 funfvbrb 5501 f1ocnv2d 5942 1stconst 6086 2ndconst 6087 cnvf1o 6090 ersymb 6411 swoer 6425 erth 6441 enen1 6702 enen2 6703 domen1 6704 domen2 6705 xpmapenlem 6711 fidifsnen 6732 fundmfibi 6795 f1dmvrnfibi 6800 ordiso2 6888 fzsplit2 9798 fseq1p1m1 9842 elfz2nn0 9860 btwnzge0 10041 modqsubdir 10134 zesq 10378 hashprg 10522 rereb 10603 abslt 10828 absle 10829 maxleastb 10954 maxltsup 10958 xrltmaxsup 10994 xrmaxltsup 10995 iserex 11076 mptfzshft 11179 fsumrev 11180 dvdsadd2b 11467 nn0ob 11532 dfgcd3 11625 dfgcd2 11629 dvdsmulgcd 11640 lcmgcdeq 11691 qden1elz 11810 cncnp 12326 xmetxpbl 12604 dedekindicc 12707 coseq0q4123 12842 coseq0negpitopi 12844 pwf1oexmid 13121 isomninnlem 13152 |
Copyright terms: Public domain | W3C validator |