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 1395 elrabf 2884 sbcco 2976 sbc5 2978 sbcan 2997 sbcor 2999 sbcal 3006 sbcex2 3008 sbcel1v 3017 eldif 3130 elun 3268 elin 3310 eluni 3797 eliun 3875 elopab 4241 opelopabsb 4243 opeliunxp 4664 opeliunxp2 4749 elxp4 5096 elxp5 5097 fsn2 5667 isocnv2 5788 elxp6 6145 elxp7 6146 opeliunxp2f 6214 brtpos2 6227 tpostpos 6240 ecdmn0m 6551 elixpsn 6709 bren 6721 omniwomnimkv 7139 elinp 7423 recexprlemell 7571 recexprlemelu 7572 gt0srpr 7697 ltresr 7788 eluz2 9480 elfz2 9959 rexanuz2 10942 even2n 11820 infssuzex 11891 infpn2 12398 istopon 12726 ishmeo 13019 ismet2 13069 |
Copyright terms: Public domain | W3C validator |