![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl13 | 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 |
---|---|
simpl13 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl3 1250 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl1 1240 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 386 ∧ w3a 1111 |
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 199 df-an 387 df-3an 1113 |
This theorem is referenced by: pythagtriplem4 15895 mply1topmatcl 20980 brbtwn2 26204 ax5seg 26237 br8 32177 nolt02o 32373 btwndiff 32662 ifscgr 32679 seglecgr12im 32745 atlatle 35388 cvlcvr1 35407 atbtwn 35514 3dimlem3 35529 3dimlem3OLDN 35530 4atlem3 35664 4atlem11 35677 4atlem12 35680 2lplnj 35688 paddasslem4 35891 paddasslem10 35897 pmodlem1 35914 llnexchb2lem 35936 pclfinclN 36018 arglem1N 36258 cdlemd4 36269 cdlemd 36275 cdleme16 36353 cdleme20 36392 cdleme21k 36406 cdleme22cN 36410 cdleme27N 36437 cdleme28c 36440 cdleme29ex 36442 cdleme32fva 36505 cdleme40n 36536 cdlemg15a 36723 cdlemg15 36724 cdlemg16ALTN 36726 cdlemg16z 36727 cdlemg20 36753 cdlemg22 36755 cdlemg29 36773 cdlemg38 36783 cdlemk56 37039 dihord2pre 37293 uzwo4 40031 fourierdlem77 41187 |
Copyright terms: Public domain | W3C validator |