Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.21nii | GIF version |
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) (Revised by Mario Carneiro, 31-Jan-2015.) |
Ref | Expression |
---|---|
pm5.21ni.1 | ⊢ (𝜑 → 𝜓) |
pm5.21ni.2 | ⊢ (𝜒 → 𝜓) |
pm5.21nii.3 | ⊢ (𝜓 → (𝜑 ↔ 𝜒)) |
Ref | Expression |
---|---|
pm5.21nii | ⊢ (𝜑 ↔ 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21ni.1 | . . . 4 ⊢ (𝜑 → 𝜓) | |
2 | pm5.21nii.3 | . . . 4 ⊢ (𝜓 → (𝜑 ↔ 𝜒)) | |
3 | 1, 2 | syl 14 | . . 3 ⊢ (𝜑 → (𝜑 ↔ 𝜒)) |
4 | 3 | ibi 175 | . 2 ⊢ (𝜑 → 𝜒) |
5 | pm5.21ni.2 | . . . 4 ⊢ (𝜒 → 𝜓) | |
6 | 5, 2 | syl 14 | . . 3 ⊢ (𝜒 → (𝜑 ↔ 𝜒)) |
7 | 6 | ibir 176 | . 2 ⊢ (𝜒 → 𝜑) |
8 | 4, 7 | impbii 125 | 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: anxordi 1363 elrabf 2811 sbcco 2903 sbc5 2905 sbcan 2923 sbcor 2925 sbcal 2932 sbcex2 2934 sbcel1v 2943 eldif 3050 elun 3187 elin 3229 eluni 3709 eliun 3787 elopab 4150 opelopabsb 4152 opeliunxp 4564 opeliunxp2 4649 elxp4 4996 elxp5 4997 fsn2 5562 isocnv2 5681 elxp6 6035 elxp7 6036 opeliunxp2f 6103 brtpos2 6116 tpostpos 6129 ecdmn0m 6439 elixpsn 6597 bren 6609 elinp 7250 recexprlemell 7398 recexprlemelu 7399 gt0srpr 7524 ltresr 7615 eluz2 9300 elfz2 9765 rexanuz2 10731 even2n 11498 infssuzex 11569 istopon 12107 ishmeo 12400 ismet2 12450 |
Copyright terms: Public domain | W3C validator |