![]() |
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: ![]() ![]() |
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 1288 elrabf 2690 sbcco 2779 sbc5 2781 sbcan 2799 sbcor 2801 sbcal 2804 sbcex2 2806 eldif 2921 elun 3078 elin 3120 eluni 3574 eliun 3652 elopab 3986 opelopabsb 3988 opeliunxp 4338 opeliunxp2 4419 elxp4 4751 elxp5 4752 fsn2 5280 isocnv2 5395 elxp6 5738 elxp7 5739 brtpos2 5807 tpostpos 5820 ecdmn0m 6084 bren 6164 elinp 6457 recexprlemell 6594 recexprlemelu 6595 gt0srpr 6676 ltresr 6736 eluz2 8255 elfz2 8651 |
Copyright terms: Public domain | W3C validator |