![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad2ant2lr | Structured version Visualization version Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.) |
Ref | Expression |
---|---|
ad2ant2.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad2ant2lr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant2.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantrr 728 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantll 725 |
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: reusv2lem2 4618 mpteqb 5986 omxpenlem 7698 fineqvlem 7811 marypha1lem 7972 fin23lem26 8780 axdc3lem4 8908 mulcmpblnr 9520 ltsrpr 9526 sub4 9944 muladd 10078 ltleadd 10124 divdivdiv 10335 divadddiv 10349 ltmul12a 10488 lt2mul2div 10510 xlemul1a 11602 fzrev 11886 facndiv 12504 fsumconst 13899 fprodconst 14080 isprm5 14699 acsfn2 15617 ghmeql 16953 subgdmdprd 17715 lssvsubcl 18215 lssvacl 18225 lidlsubclOLD 18488 ocvin 19285 lindfmm 19433 scmatghm 19606 scmatmhm 19607 slesolinv 19753 slesolinvbi 19754 slesolex 19755 pm2mpf1lem 19866 pm2mpcoe1 19872 reftr 20577 alexsubALTlem2 21111 alexsubALTlem3 21112 blbas 21493 nmoco 21806 cncfmet 21988 cmetcaulem 22306 mbflimsup 22671 mbflimsupOLD 22672 ulmdvlem3 23405 ptolemy 23499 grpoideu 25985 ipblnfi 26545 htthlem 26618 hvaddsub4 26779 bralnfn 27649 hmops 27721 hmopm 27722 adjadd 27794 opsqrlem1 27841 atomli 28083 chirredlem2 28092 atcvat3i 28097 mdsymlem5 28108 cdj1i 28134 derangenlem 29942 elmrsubrn 30206 dfon2lem6 30482 poseq 30539 sltsolem1 30605 mblfinlem1 32021 prdsbnd 32169 heibor1lem 32185 hl2at 33014 congneg 35863 jm2.26 35901 stoweidlem34 37932 31wlkdlem6 39905 lindslinindsimp2 40528 ltsubaddb 40583 ltsubadd2b 40585 aacllem 40812 |
Copyright terms: Public domain | W3C validator |