![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr32 | Structured version Visualization version GIF version |
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.) |
Ref | Expression |
---|---|
simpr32 | ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr2 1195 | . 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
2 | 1 | 3ad2antr3 1190 | 1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1087 |
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 206 df-an 397 df-3an 1089 |
This theorem is referenced by: oppccatid 17661 subccatid 17792 fuccatid 17918 setccatid 18030 catccatid 18052 estrccatid 18079 xpccatid 18136 nllyidm 22984 utoptop 23730 omndmul2 32217 cgr3tr4 35012 paddasslem9 38687 cdlemd1 39057 cdlemf2 39421 cdlemk34 39769 dihmeetlem18N 40183 isthincd2 47611 mndtccatid 47666 |
Copyright terms: Public domain | W3C validator |