![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3adant3r3 | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 18-Feb-2008.) |
Ref | Expression |
---|---|
3exp.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3adant3r3 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3exp.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | 3expb 1216 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3adantr3 1175 |
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 df-3an 993 |
This theorem is referenced by: ressress 15242 plttr 16271 plelttr 16273 latledi 16390 latmlej11 16391 latmlej21 16393 latmlej22 16394 latjass 16396 latj12 16397 latj31 16400 ipopos 16461 latdisdlem 16490 imasmnd2 16628 imasmnd 16629 grpaddsubass 16799 grpsubsub4 16802 grpnpncan 16804 imasgrp2 16856 imasgrp 16857 frgp0 17465 cmn12 17505 abladdsub 17512 imasring 17902 dvrass 17973 lss1 18217 islmhm2 18316 psrgrp 18677 psrlmod 18680 zntoslem 19182 ipdir 19261 t1sep 20441 mettri2 21411 xmetrtri 21425 xmetrtri2 21426 pi1grplem 22135 dchrabl 24238 motgrp 24644 xmstrkgc 24972 ax5seglem4 25018 grpomuldivass 26033 grpopnpcan2 26037 grponpncan 26039 grpodiveq 26040 ablomuldiv 26073 ablodivdiv4 26075 nvadd12 26298 nvmdi 26327 nvsubadd 26332 nvmtri2 26357 dipdi 26540 dipsubdir 26545 dipsubdi 26546 cgr3tr4 30869 cgr3rflx 30871 seglemin 30930 linerflx1 30966 elicc3 31023 rngosubdi 32238 rngosubdir 32239 igenval2 32345 dmncan1 32355 latmassOLD 32841 omlfh1N 32870 omlfh3N 32871 cvrnbtwn 32883 cvrnbtwn2 32887 cvrnbtwn4 32891 hlatj12 32982 cvrntr 33036 islpln2a 33159 3atnelvolN 33197 elpadd2at2 33418 paddasslem17 33447 paddass 33449 paddssw2 33455 pmapjlln1 33466 ltrn2ateq 33792 cdlemc3 33805 cdleme1b 33838 cdleme3b 33841 cdleme3c 33842 cdleme9b 33864 erngdvlem3 34603 erngdvlem3-rN 34611 dvalveclem 34639 mendlmod 36105 lincsumscmcl 40595 |
Copyright terms: Public domain | W3C validator |