![]() |
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 176 | . 2 ⊢ (𝜑 → 𝜒) |
5 | pm5.21ni.2 | . . . 4 ⊢ (𝜒 → 𝜓) | |
6 | 5, 2 | syl 14 | . . 3 ⊢ (𝜒 → (𝜑 ↔ 𝜒)) |
7 | 6 | ibir 177 | . 2 ⊢ (𝜒 → 𝜑) |
8 | 4, 7 | impbii 126 | 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: anxordi 1410 elrabf 2903 sbcco 2996 sbc5 2998 sbcan 3017 sbcor 3019 sbcal 3026 sbcex2 3028 sbcel1v 3037 eldif 3150 elun 3288 elin 3330 eluni 3824 eliun 3902 elopab 4270 opelopabsb 4272 opeliunxp 4693 opeliunxp2 4779 elxp4 5128 elxp5 5129 fsn2 5703 isocnv2 5826 elxp6 6183 elxp7 6184 opeliunxp2f 6252 brtpos2 6265 tpostpos 6278 ecdmn0m 6590 elixpsn 6748 bren 6760 omniwomnimkv 7178 elinp 7486 recexprlemell 7634 recexprlemelu 7635 gt0srpr 7760 ltresr 7851 eluz2 9547 elfz2 10028 rexanuz2 11013 even2n 11892 infssuzex 11963 infpn2 12470 xpsfrnel2 12783 issubg 13064 isnsg 13093 issrg 13212 iscrng2 13262 issubrng 13414 issubrg 13436 islssm 13541 islidlm 13663 2idlelb 13684 istopon 13784 ishmeo 14075 ismet2 14125 |
Copyright terms: Public domain | W3C validator |