![]() |
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 1194 | . 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜓) | |
2 | 1 | 3ad2antr3 1189 | 1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜓) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 207 df-an 396 df-3an 1088 |
This theorem is referenced by: oppccatid 17766 subccatid 17897 fuccatid 18026 setccatid 18138 catccatid 18160 estrccatid 18187 xpccatid 18244 nllyidm 23513 utoptop 24259 omndmul2 33072 cgr3tr4 36034 paddasslem9 39811 cdlemd1 40181 cdlemf2 40545 cdlemk34 40893 dihmeetlem18N 41307 isthincd2 48838 mndtccatid 48896 |
Copyright terms: Public domain | W3C validator |