![]() |
New Foundations Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > NFE Home > Th. List > pm5.21nii | Unicode version |
Description: Eliminate an antecedent implied by each side of a biconditional. (Contributed by NM, 21-May-1999.) |
Ref | Expression |
---|---|
pm5.21ni.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
pm5.21ni.2 |
![]() ![]() ![]() ![]() ![]() ![]() |
pm5.21nii.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm5.21nii |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21nii.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm5.21ni.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
3 | pm5.21ni.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 2, 3 | pm5.21ni 341 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 1, 4 | pm2.61i 156 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 |
This theorem is referenced by: elrabf 2993 sbcco 3068 sbc5 3070 sbcan 3088 sbcor 3090 sbcal 3093 sbcex2 3095 elin 3219 elun 3220 eluni 3894 eliun 3973 el1c 4139 elxpk 4196 eladdc 4398 elopab 4696 opelopabsb 4697 elima 4754 brsi 4761 epelc 4765 opeliunxp 4820 opeliunxp2 4822 br1st 4858 br2nd 4859 brswap2 4860 brco 4883 brcnv 4892 elimasn 5019 opbr1st 5501 opbr2nd 5502 brswap 5509 trtxp 5781 elfix 5787 otelins2 5791 otelins3 5792 oqelins4 5794 brfns 5833 qrpprod 5836 fnfullfunlem1 5856 bren 6030 enpw1 6062 brltc 6114 elncs 6119 elnc 6125 ncseqnc 6128 elcan 6329 elscan 6330 |
Copyright terms: Public domain | W3C validator |