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 1185 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl1 1177 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1079 |
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 208 df-an 397 df-3an 1081 |
This theorem is referenced by: pythagtriplem4 16146 mply1topmatcl 21343 brbtwn2 26619 ax5seg 26652 br8 32890 nolt02o 33097 btwndiff 33386 ifscgr 33403 seglecgr12im 33469 atlatle 36338 cvlcvr1 36357 atbtwn 36464 3dimlem3 36479 3dimlem3OLDN 36480 4atlem3 36614 4atlem11 36627 4atlem12 36630 2lplnj 36638 paddasslem4 36841 paddasslem10 36847 pmodlem1 36864 llnexchb2lem 36886 pclfinclN 36968 arglem1N 37208 cdlemd4 37219 cdlemd 37225 cdleme16 37303 cdleme20 37342 cdleme21k 37356 cdleme22cN 37360 cdleme27N 37387 cdleme28c 37390 cdleme29ex 37392 cdleme32fva 37455 cdleme40n 37486 cdlemg15a 37673 cdlemg15 37674 cdlemg16ALTN 37676 cdlemg16z 37677 cdlemg20 37703 cdlemg22 37705 cdlemg29 37723 cdlemg38 37733 cdlemk56 37989 dihord2pre 38243 ismnu 40477 uzwo4 41195 fourierdlem77 42349 |
Copyright terms: Public domain | W3C validator |