![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
Mirrors > Home > MPE Home > Th. List > pm5.21ndd | 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 133 | . . 3 |
4 | pm5.21ndd.2 | . . . 4 | |
5 | 4 | con3d 133 | . . 3 |
6 | pm5.21im 349 | . . 3 | |
7 | 3, 5, 6 | syl6c 64 | . 2 |
8 | 1, 7 | pm2.61d 158 | 1 |
Colors of variables: wff setvar class |
Syntax hints: -. wn 3 -> wi 4
<-> wb 184 |
This theorem is referenced by: pm5.21nd 900 rmob 3430 oteqex 4745 epelg 4797 eqbrrdva 5177 relbrcnvg 5380 ordsucuniel 6659 ordsucun 6660 brtpos2 6980 eceqoveq 7435 elpmg 7454 elfi2 7894 brwdom 8014 brwdomn0 8016 rankr1c 8260 r1pwcl 8286 ttukeylem1 8910 fpwwe2lem9 9037 eltskm 9242 recmulnq 9363 clim 13317 rlim 13318 lo1o1 13355 o1lo1 13360 o1lo12 13361 rlimresb 13388 lo1eq 13391 rlimeq 13392 isercolllem2 13488 caucvgb 13502 saddisj 14115 sadadd 14117 sadass 14121 bitsshft 14125 smupvallem 14133 smumul 14143 catpropd 15104 isssc 15189 issubc 15204 funcres2b 15266 funcres2c 15270 mndpropd 15946 issubg3 16219 resghm2b 16285 resscntz 16369 elsymgbas 16407 odmulg 16578 dmdprd 17029 dprdw 17043 dprdwOLD 17050 subgdmdprd 17081 lmodprop2d 17572 lssacs 17613 assapropd 17976 psrbaglefi 18023 psrbaglefiOLD 18024 prmirred 18525 prmirredOLD 18528 lindfmm 18862 lsslindf 18865 islinds3 18869 cnrest2 19787 cnprest 19790 cnprest2 19791 lmss 19799 isfildlem 20358 isfcls 20510 elutop 20736 metustelOLD 21054 metustel 21055 blval2 21078 dscopn 21094 iscau2 21716 causs 21737 ismbf 22037 ismbfcn 22038 iblcnlem 22195 limcdif 22280 limcres 22290 limcun 22299 dvres 22315 q1peqb 22555 ulmval 22775 ulmres 22783 chpchtsum 23494 dchrisum0lem1 23701 axcontlem5 24271 iseupa 24965 ismndo2 25347 isrngo 25380 issiga 28111 ismeas 28170 cvmlift3lem4 28767 msrrcl 28903 brcolinear2 29708 topfneec 30173 cnpwstotbnd 30293 ismtyima 30299 elrfi 30626 climf 31628 lshpkr 34842 |
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 185 |
Copyright terms: Public domain | W3C validator |