Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > simpr33 | 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 |
---|---|
simpr33 | ⊢ ((𝜂 ∧ (𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpr3 1192 | . 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 16991 subccatid 17118 fuccatid 17241 setccatid 17346 catccatid 17364 estrccatid 17384 xpccatid 17440 nllyidm 22099 utoptop 22845 cgr3tr4 33515 paddasslem9 36966 cdlemd1 37336 cdlemf2 37700 cdlemk34 38048 dihmeetlem18N 38462 dihmeetlem19N 38463 |
Copyright terms: Public domain | W3C validator |