![]() |
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 1191 | . 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒) | |
2 | 1 | 3ad2antl1 1183 | 1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1085 |
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 206 df-an 396 df-3an 1087 |
This theorem is referenced by: pythagtriplem4 16787 mply1topmatcl 22706 nolt02o 27627 nogt01o 27628 cofsslt 27837 coinitsslt 27838 brbtwn2 28715 ax5seg 28748 br8 35350 btwndiff 35623 ifscgr 35640 seglecgr12im 35706 atlatle 38792 cvlcvr1 38811 atbtwn 38919 3dimlem3 38934 3dimlem3OLDN 38935 4atlem3 39069 4atlem11 39082 4atlem12 39085 2lplnj 39093 paddasslem4 39296 paddasslem10 39302 pmodlem1 39319 llnexchb2lem 39341 pclfinclN 39423 arglem1N 39663 cdlemd4 39674 cdlemd 39680 cdleme16 39758 cdleme20 39797 cdleme21k 39811 cdleme22cN 39815 cdleme27N 39842 cdleme28c 39845 cdleme29ex 39847 cdleme32fva 39910 cdleme40n 39941 cdlemg15a 40128 cdlemg15 40129 cdlemg16ALTN 40131 cdlemg16z 40132 cdlemg20 40158 cdlemg22 40160 cdlemg29 40178 cdlemg38 40188 cdlemk56 40444 dihord2pre 40698 ismnu 43698 uzwo4 44417 fourierdlem77 45571 |
Copyright terms: Public domain | W3C validator |