![]() |
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 115 | . 2 ⊢ (𝜑 → (𝜓 → 𝜒)) |
3 | impbida.2 | . . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜓) | |
4 | 3 | ex 115 | . 2 ⊢ (𝜑 → (𝜒 → 𝜓)) |
5 | 2, 4 | impbid 129 | 1 ⊢ (𝜑 → (𝜓 ↔ 𝜒)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: eqrdav 2176 funfvbrb 5624 f1ocnv2d 6068 1stconst 6215 2ndconst 6216 cnvf1o 6219 ersymb 6542 swoer 6556 erth 6572 enen1 6833 enen2 6834 domen1 6835 domen2 6836 xpmapenlem 6842 fidifsnen 6863 fundmfibi 6931 f1dmvrnfibi 6936 ordiso2 7027 omniwomnimkv 7158 enwomnilem 7160 nninfwlpoimlemginf 7167 infregelbex 9574 fzsplit2 10023 fseq1p1m1 10067 elfz2nn0 10085 btwnzge0 10273 modqsubdir 10366 zesq 10611 hashprg 10759 rereb 10843 abslt 11068 absle 11069 maxleastb 11194 maxltsup 11198 xrltmaxsup 11236 xrmaxltsup 11237 iserex 11318 mptfzshft 11421 fsumrev 11422 fprodrev 11598 dvdsadd2b 11818 nn0ob 11883 dfgcd3 11981 dfgcd2 11985 dvdsmulgcd 11996 lcmgcdeq 12053 isprm5 12112 qden1elz 12175 issubmnd 12722 mhmf1o 12738 grpinvid1 12801 grpinvid2 12802 0unit 13110 cncnp 13363 xmetxpbl 13641 dedekindicc 13744 coseq0q4123 13888 coseq0negpitopi 13890 relogeftb 13919 relogbcxpbap 14016 pwf1oexmid 14371 isomninnlem 14401 apdiff 14419 iswomninnlem 14420 ismkvnnlem 14423 redcwlpolemeq1 14425 |
Copyright terms: Public domain | W3C validator |