![]() |
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 178 | . 2 ⊢ (𝜑 → (𝜒 → 𝜃)) |
5 | pm5.21ndd.2 | . . . . 5 ⊢ (𝜑 → (𝜃 → 𝜓)) | |
6 | 5, 2 | syld 45 | . . . 4 ⊢ (𝜑 → (𝜃 → (𝜒 ↔ 𝜃))) |
7 | bicom1 131 | . . . 4 ⊢ ((𝜒 ↔ 𝜃) → (𝜃 ↔ 𝜒)) | |
8 | 6, 7 | syl6 33 | . . 3 ⊢ (𝜑 → (𝜃 → (𝜃 ↔ 𝜒))) |
9 | 8 | ibd 178 | . 2 ⊢ (𝜑 → (𝜃 → 𝜒)) |
10 | 4, 9 | impbid 129 | 1 ⊢ (𝜑 → (𝜒 ↔ 𝜃)) |
Colors of variables: wff set class |
Syntax hints: → wi 4 ↔ wb 105 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 |
This theorem depends on definitions: df-bi 117 |
This theorem is referenced by: pm5.21nd 916 sbcrext 3040 rmob 3055 epelg 4290 eqbrrdva 4797 elrelimasn 4994 relbrcnvg 5007 fmptco 5682 ovelrn 6022 brtpos2 6251 elpmg 6663 brdomg 6747 elfi2 6970 genpelvl 7510 genpelvu 7511 fzoval 10145 clim 11284 pceu 12289 mndpropd 12795 issubg3 13005 dvdsrd 13216 subrgpropd 13329 cnrest2 13629 cnptoprest2 13633 lmss 13639 reopnap 13931 limcdifap 14024 |
Copyright terms: Public domain | W3C validator |