Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3ad2antr3 | Structured version Visualization version Unicode version |
Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 30-Dec-2007.) |
Ref | Expression |
---|---|
3ad2antl.1 |
Ref | Expression |
---|---|
3ad2antr3 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3ad2antl.1 | . . 3 | |
2 | 1 | adantrl 752 | . 2 |
3 | 2 | 3adantr1 1220 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 384 w3a 1037 |
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 197 df-an 386 df-3an 1039 |
This theorem is referenced by: fpr2g 6475 frfi 8205 ressress 15938 funcestrcsetclem9 16788 funcsetcestrclem9 16803 latjjdir 17104 grprcan 17455 grpsubrcan 17496 grpaddsubass 17505 mhmmnd 17537 zntoslem 19905 ipdir 19984 ipass 19990 qustgpopn 21923 grpomuldivass 27395 nvmdi 27503 dmdsl3 29174 dvrcan5 29793 esum2d 30155 voliune 30292 btwnconn1lem7 32200 poimirlem4 33413 cvrnbtwn4 34566 paddasslem14 35119 paddasslem17 35122 paddss 35131 pmod1i 35134 cdleme1 35514 cdleme2 35515 xlimbr 40053 sbgoldbst 41666 funcringcsetcALTV2lem9 42044 funcringcsetclem9ALTV 42067 |
Copyright terms: Public domain | W3C validator |