New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > ad2antrr | Unicode version |
Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.) (Proof shortened by Wolf Lammen, 20-Nov-2012.) |
Ref | Expression |
---|---|
ad2ant.1 |
Ref | Expression |
---|---|
ad2antrr |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 | . . 3 | |
2 | 1 | adantr 451 | . 2 |
3 | 2 | adantlr 695 | 1 |
Colors of variables: wff setvar class |
Syntax hints: wi 4 wa 358 |
This theorem was proved from axioms: ax-1 5 ax-2 6 ax-3 7 ax-mp 8 |
This theorem depends on definitions: df-bi 177 df-an 360 |
This theorem is referenced by: ad3antrrr 710 simpll 730 simplll 734 simpllr 735 ax11eq 2193 ax11el 2194 ax11indalem 2197 ax11inda2ALT 2198 vtoclgft 2905 reupick 3539 ltfinasym 4460 sfinltfin 4535 vfinspsslem1 4550 isotr 5495 qsdisj 5995 nntccl 6170 sbthlem3 6205 ltlenlec 6207 letc 6231 ncslemuc 6255 fnfrec 6320 |
Copyright terms: Public domain | W3C validator |