![]() |
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 1192 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl1 1184 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 |
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 1088 |
This theorem is referenced by: pythagtriplem4 16853 mply1topmatcl 22827 nolt02o 27755 nogt01o 27756 cofsslt 27967 coinitsslt 27968 brbtwn2 28935 ax5seg 28968 br8 35736 btwndiff 36009 ifscgr 36026 seglecgr12im 36092 atlatle 39302 cvlcvr1 39321 atbtwn 39429 3dimlem3 39444 3dimlem3OLDN 39445 4atlem3 39579 4atlem11 39592 4atlem12 39595 2lplnj 39603 paddasslem4 39806 paddasslem10 39812 pmodlem1 39829 llnexchb2lem 39851 pclfinclN 39933 arglem1N 40173 cdlemd4 40184 cdlemd 40190 cdleme16 40268 cdleme20 40307 cdleme21k 40321 cdleme22cN 40325 cdleme27N 40352 cdleme28c 40355 cdleme29ex 40357 cdleme32fva 40420 cdleme40n 40451 cdlemg15a 40638 cdlemg15 40639 cdlemg16ALTN 40641 cdlemg16z 40642 cdlemg20 40668 cdlemg22 40670 cdlemg29 40688 cdlemg38 40698 cdlemk56 40954 dihord2pre 41208 ismnu 44257 uzwo4 44993 fourierdlem77 46139 |
Copyright terms: Public domain | W3C validator |