![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > simpl12 | 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 |
---|---|
simpl12 | ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpl2 1191 | . 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 pmatcollpw1lem1 22796 pmatcollpw1 22798 mp2pm2mplem2 22829 nolt02o 27755 nogt01o 27756 brbtwn2 28935 ax5seg 28968 3vfriswmgr 30307 br8 35736 ifscgr 36026 seglecgr12im 36092 lkrshp 39087 atlatle 39302 cvlcvr1 39321 atbtwn 39429 3dimlem3 39444 3dimlem3OLDN 39445 1cvratex 39456 llnmlplnN 39522 4atlem3 39579 4atlem3a 39580 4atlem11 39592 4atlem12 39595 cdlemb 39777 paddasslem4 39806 paddasslem10 39812 pmodlem1 39829 llnexchb2lem 39851 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 cdlemk33N 40892 cdlemk56 40954 fourierdlem77 46139 |
Copyright terms: Public domain | W3C validator |