![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad6antr | Structured version Visualization version Unicode version |
Description: Deduction adding 6 conjuncts to antecedent. (Contributed by Mario Carneiro, 4-Jan-2017.) |
Ref | Expression |
---|---|
ad2ant.1 |
![]() ![]() ![]() ![]() ![]() ![]() |
Ref | Expression |
---|---|
ad6antr |
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ad2ant.1 |
. . 3
![]() ![]() ![]() ![]() ![]() ![]() | |
2 | 1 | ad5antr 745 |
. 2
![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() ![]() |
3 | 2 | adantr 471 |
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 |
This theorem is referenced by: ad7antr 749 catass 15641 funcpropd 15854 natpropd 15930 restutop 21301 utopreg 21316 restmetu 21634 lgamucov 24012 istrkgcb 24553 tgifscgr 24602 tgbtwnconn1lem3 24668 legtrd 24683 miriso 24764 footex 24812 opphllem3 24840 opphl 24845 trgcopy 24895 cgratr 24914 dfcgra2 24920 inaghl 24930 cgrg3col4 24933 f1otrge 24951 cusgrares 25249 clwlkisclwwlklem1 25564 heicant 32020 mblfinlem3 32024 limclner 37770 hoidmvle 38460 |
Copyright terms: Public domain | W3C validator |