Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.21ndd | GIF version |
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm5.21ndd.1 | ⊢ (𝜑 → (𝜒 → 𝜓)) |
pm5.21ndd.2 | ⊢ (𝜑 → (𝜃 → 𝜓)) |
pm5.21ndd.3 | ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) |
Ref | Expression |
---|---|
pm5.21ndd | ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21ndd.1 | . . . 4 ⊢ (𝜑 → (𝜒 → 𝜓)) | |
2 | pm5.21ndd.3 | . . . 4 ⊢ (𝜑 → (𝜓 → (𝜒 ↔ 𝜃))) | |
3 | 1, 2 | syld 45 | . . 3 ⊢ (𝜑 → (𝜒 → (𝜒 ↔ 𝜃))) |
4 | 3 | ibd 177 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | pm5.21ndd.2 | . . . . 5 ⊢ (𝜑 → (𝜃 → 𝜓)) | |
6 | 5, 2 | syld 45 | . . . 4 ⊢ (𝜑 → (𝜃 → (𝜒 ↔ 𝜃))) |
7 | bicom1 130 | . . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 ↔ 𝜒)) | |
8 | 6, 7 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜃 → (𝜃 ↔ 𝜒))) |
9 | 8 | ibd 177 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
10 | 4, 9 | impbid 128 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 104 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: pm5.21nd 901 sbcrext 2986 rmob 3001 epelg 4212 eqbrrdva 4709 relbrcnvg 4918 fmptco 5586 ovelrn 5919 brtpos2 6148 elpmg 6558 brdomg 6642 elfi2 6860 genpelvl 7320 genpelvu 7321 fzoval 9925 clim 11050 cnrest2 12405 cnptoprest2 12409 lmss 12415 reopnap 12707 limcdifap 12800 |
Copyright terms: Public domain | W3C validator |