Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > pm5.21nii | Unicode 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 165 | . 2 |
5 | pm5.21ni.2 | . . . 4 | |
6 | 5, 2 | syl 14 | . . 3 |
7 | 6 | ibir 166 | . 2 |
8 | 4, 7 | impbii 117 | 1 |
Colors of variables: wff set class |
Syntax hints: wi 4 wb 98 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-mp 7 ax-ia1 99 ax-ia2 100 ax-ia3 101 |
This theorem depends on definitions: df-bi 110 |
This theorem is referenced by: anxordi 1291 elrabf 2696 sbcco 2785 sbc5 2787 sbcan 2805 sbcor 2807 sbcal 2810 sbcex2 2812 eldif 2927 elun 3084 elin 3126 eluni 3583 eliun 3661 elopab 3995 opelopabsb 3997 opeliunxp 4395 opeliunxp2 4476 elxp4 4808 elxp5 4809 fsn2 5337 isocnv2 5452 elxp6 5796 elxp7 5797 brtpos2 5866 tpostpos 5879 ecdmn0m 6148 bren 6228 elinp 6572 recexprlemell 6720 recexprlemelu 6721 gt0srpr 6833 ltresr 6915 eluz2 8479 elfz2 8881 rexanuz2 9589 |
Copyright terms: Public domain | W3C validator |