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 1190 | . 2 ⊢ ((𝜂 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) → 𝜑) | |
2 | 1 | 3ad2antr3 1186 | 1 ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜑) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 398 ∧ w3a 1083 |
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 209 df-an 399 df-3an 1085 |
This theorem is referenced by: oppccatid 16983 subccatid 17110 fuccatid 17233 setccatid 17338 catccatid 17356 estrccatid 17376 xpccatid 17432 nllyidm 22091 utoptop 22837 cgr3tr4 33508 seglecgr12im 33566 paddasslem9 36958 cdlemd1 37328 cdlemf2 37692 cdlemk34 38040 dihmeetlem18N 38454 dihmeetlem19N 38455 |
Copyright terms: Public domain | W3C validator |