![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > ad6antr | Structured version Visualization version GIF 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 766 | . 2 ⊢ ((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) → 𝜓) |
3 | 2 | adantr 480 | 1 ⊢ (((((((𝜑 ∧ 𝜒) ∧ 𝜃) ∧ 𝜏) ∧ 𝜂) ∧ 𝜁) ∧ 𝜎) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 383 |
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 196 df-an 385 |
This theorem is referenced by: ad7antr 770 catass 16170 funcpropd 16383 natpropd 16459 restutop 21851 utopreg 21866 restmetu 22185 lgamucov 24564 istrkgcb 25155 tgifscgr 25203 tgbtwnconn1lem3 25269 legtrd 25284 miriso 25365 footex 25413 opphllem3 25441 opphl 25446 trgcopy 25496 cgratr 25515 dfcgra2 25521 inaghl 25531 cgrg3col4 25534 f1otrge 25552 cusgrares 26001 clwlkisclwwlklem1 26315 matunitlindflem1 32575 heicant 32614 mblfinlem3 32618 limclner 38718 hoidmvle 39490 clwlkclwwlklem2 41209 |
Copyright terms: Public domain | W3C validator |