Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > 3adant3l | Structured version Visualization version Unicode version |
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 8-Jan-2006.) |
Ref | Expression |
---|---|
3adant1l.1 |
Ref | Expression |
---|---|
3adant3l |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3adant1l.1 | . . . 4 | |
2 | 1 | 3com13 1270 | . . 3 |
3 | 2 | 3adant1l 1318 | . 2 |
4 | 3 | 3com13 1270 | 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: wfrlem12 7426 ecopovtrn 7850 rrxmet 23191 nvaddsub4 27512 adjlnop 28945 pl1cn 30001 frrlem11 31792 rrnmet 33628 lflsub 34354 lflmul 34355 cvlatexch3 34625 cdleme5 35527 cdlemeg46rjgN 35810 cdlemg2l 35891 cdlemg10c 35927 tendospcanN 36312 dicvaddcl 36479 dicvscacl 36480 dochexmidlem8 36756 limsupre3lem 39964 fourierdlem42 40366 fourierdlem113 40436 ovnsupge0 40771 ovncvrrp 40778 ovnhoilem2 40816 |
Copyright terms: Public domain | W3C validator |