![]() |
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 3042 rmob 3057 epelg 4292 eqbrrdva 4799 elrelimasn 4996 relbrcnvg 5009 fmptco 5684 ovelrn 6025 brtpos2 6254 elpmg 6666 brdomg 6750 elfi2 6973 genpelvl 7513 genpelvu 7514 fzoval 10150 clim 11291 dvdsaddre2b 11850 pceu 12297 mndpropd 12846 issubg3 13057 dvdsrd 13268 subrgpropd 13374 lmodprop2d 13443 cnrest2 13821 cnptoprest2 13825 lmss 13831 reopnap 14123 limcdifap 14216 |
Copyright terms: Public domain | W3C validator |