![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm2.61ian | Structured version Visualization version Unicode version |
Description: Elimination of an antecedent. (Contributed by NM, 1-Jan-2005.) |
Ref | Expression |
---|---|
pm2.61ian.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm2.61ian.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm2.61ian |
![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2.61ian.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ex 440 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | pm2.61ian.2 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
4 | 3 | ex 440 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
5 | 2, 4 | pm2.61i 169 |
1
![]() ![]() ![]() ![]() ![]() ![]() |
Colors of variables: wff setvar class |
Syntax hints: ![]() ![]() ![]() |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 190 df-an 377 |
This theorem is referenced by: 4cases 966 consensus 976 cases2 989 sbcrext 3352 csbexg 4550 xpcan2 5292 tfindsg 6713 findsg 6746 ixpexg 7571 fipwss 7968 ranklim 8340 fin23lem14 8788 fzoval 11951 hashge2el2dif 12669 iswrdi 12707 ffz0iswrd 12729 swrd0 12826 swrdsbslen 12840 swrdspsleq 12841 swrdccatin12 12883 swrdccat 12885 repswswrd 12923 cshword 12929 cshwcsh2id 12963 lcmftp 14657 prmop1 15044 fvprmselelfz 15050 ressbas 15227 resslem 15230 ressinbas 15233 cntzval 17023 symg2bas 17087 sralem 18448 srasca 18452 sravsca 18453 sraip 18454 ocvval 19278 dsmmval 19345 dmatmul 19570 1mavmul 19621 mavmul0g 19626 1marepvmarrepid 19648 smadiadetglem2 19745 1elcpmat 19787 decpmatid 19842 tnglem 21696 tngds 21704 clwlkisclwwlklem2a4 25560 clwlkisclwwlklem2a 25561 clwwisshclwwn 25584 unopbd 27716 nmopcoi 27796 resvsca 28641 resvlem 28642 ax12indalem 32560 afvres 38711 afvco2 38715 pfxccatin12 39005 pfxccat3a 39009 cshword2 39017 2ffzoeq 39105 uvtxa01vtx 39519 ply1mulgsumlem2 40451 lcoel0 40493 lindslinindsimp1 40522 difmodm1lt 40597 digexp 40690 dig1 40691 |
Copyright terms: Public domain | W3C validator |