![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > 3ad2antr2 | Structured version Visualization version Unicode version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 27-Dec-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
3ad2antr2 |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | adantrl 730 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | 3adantr3 1191 |
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 378 df-3an 1009 |
This theorem is referenced by: axdc4lem 8903 ioc0 11708 funcestrcsetclem9 16111 funcsetcestrclem9 16126 grpsubadd 16820 psrbaglesupp 18669 zntoslem 19204 trcfilu 21387 constr2wlk 25407 constr2trl 25408 constr3trllem1 25457 grpopnpcan2 26062 mdsl3 28050 dvrcan5 28630 brofs2 30915 brifs2 30916 poimirlem28 32032 ftc1anc 32089 frinfm 32126 welb 32127 fdc 32138 unichnidl 32328 cvrnbtwn2 32912 islpln2a 33184 paddss1 33453 paddss2 33454 paddasslem17 33472 tendospass 34658 funcringcsetcALTV2lem9 40554 funcringcsetclem9ALTV 40577 ldepsprlem 40773 |
Copyright terms: Public domain | W3C validator |