![]() |
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-1 5 ax-2 6 ax-mp 7 ax-ia1 105 ax-ia2 106 ax-ia3 107 |
This theorem depends on definitions: df-bi 116 |
This theorem is referenced by: anxordi 1343 elrabf 2783 sbcco 2875 sbc5 2877 sbcan 2895 sbcor 2897 sbcal 2904 sbcex2 2906 sbcel1v 2915 eldif 3022 elun 3156 elin 3198 eluni 3678 eliun 3756 elopab 4109 opelopabsb 4111 opeliunxp 4522 opeliunxp2 4607 elxp4 4952 elxp5 4953 fsn2 5510 isocnv2 5629 elxp6 5978 elxp7 5979 opeliunxp2f 6041 brtpos2 6054 tpostpos 6067 ecdmn0m 6374 elixpsn 6532 bren 6544 elinp 7130 recexprlemell 7278 recexprlemelu 7279 gt0srpr 7391 ltresr 7473 eluz2 9124 elfz2 9580 rexanuz2 10539 even2n 11301 infssuzex 11372 istopon 11864 ismet2 12140 |
Copyright terms: Public domain | W3C validator |