![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpr31 | 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 |
---|---|
simpr31 | ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr1 1194 | . 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | 3ad2antr3 1190 | 1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ 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 207 df-an 396 df-3an 1089 |
This theorem is referenced by: oppccatid 17779 subccatid 17910 fuccatid 18039 setccatid 18151 catccatid 18173 estrccatid 18200 xpccatid 18257 nllyidm 23518 utoptop 24264 cgr3tr4 36016 seglecgr12im 36074 paddasslem9 39785 cdlemd1 40155 cdlemf2 40519 cdlemk34 40867 dihmeetlem18N 41281 dihmeetlem19N 41282 isthincd2 48705 mndtccatid 48760 |
Copyright terms: Public domain | W3C validator |