![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pm5.21ndd | Structured version Visualization version Unicode version |
Description: Eliminate an antecedent implied by each side of a biconditional, deduction version. (Contributed by Paul Chapman, 21-Nov-2012.) (Proof shortened by Wolf Lammen, 6-Oct-2013.) |
Ref | Expression |
---|---|
pm5.21ndd.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm5.21ndd.2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
pm5.21ndd.3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
pm5.21ndd |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm5.21ndd.3 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | pm5.21ndd.1 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
3 | 2 | con3d 139 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
4 | pm5.21ndd.2 |
. . . 4
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
5 | 4 | con3d 139 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
6 | pm5.21im 351 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
7 | 3, 5, 6 | syl6c 66 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
8 | 1, 7 | pm2.61d 162 |
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 189 |
This theorem is referenced by: pm5.21nd 910 rmob 3358 oteqex 4693 epelg 4745 eqbrrdva 5003 relbrcnvg 5207 ordsucuniel 6648 ordsucun 6649 brtpos2 6976 eceqoveq 7465 elpmg 7484 elfi2 7925 brwdom 8079 brwdomn0 8081 rankr1c 8289 r1pwcl 8315 ttukeylem1 8936 fpwwe2lem9 9060 eltskm 9265 recmulnq 9386 clim 13551 rlim 13552 lo1o1 13589 o1lo1 13594 o1lo12 13595 rlimresb 13622 lo1eq 13625 rlimeq 13626 isercolllem2 13722 caucvgb 13739 saddisj 14432 sadadd 14434 sadass 14438 bitsshft 14442 smupvallem 14450 smumul 14460 catpropd 15607 isssc 15718 issubc 15733 funcres2b 15795 funcres2c 15799 mndpropd 16555 issubg3 16828 resghm2b 16894 resscntz 16978 elsymgbas 17016 odmulg 17200 dmdprd 17623 dprdw 17635 subgdmdprd 17660 lmodprop2d 18143 lssacs 18183 assapropd 18544 psrbaglefi 18589 prmirred 19059 lindfmm 19378 lsslindf 19381 islinds3 19385 cnrest2 20295 cnprest 20298 cnprest2 20299 lmss 20307 isfildlem 20865 isfcls 21017 elutop 21241 metustel 21558 blval2 21570 dscopn 21581 iscau2 22240 causs 22261 ismbf 22579 ismbfcn 22580 iblcnlem 22739 limcdif 22824 limcres 22834 limcun 22843 dvres 22859 q1peqb 23098 ulmval 23328 ulmres 23336 chpchtsum 24140 dchrisum0lem1 24347 axcontlem5 24991 iseupa 25686 ismndo2 26066 isrngo 26099 issiga 28926 ismeas 29014 elcarsg 29130 cvmlift3lem4 30038 msrrcl 30174 brcolinear2 30818 topfneec 31004 cnpwstotbnd 32122 ismtyima 32128 lshpkr 32677 elrfi 35530 climf 37696 is1wlkg 39614 |
Copyright terms: Public domain | W3C validator |