Theorem simpl13 1251

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl13	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl13

Step	Hyp	Ref	Expression
1		simpl3 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl1 1186	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

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  16839  mply1topmatcl  22743  nolt02o  27659  nogt01o  27660  cofsslt  27878  coinitsslt  27879  brbtwn2  28884  ax5seg  28917  br8  35773  btwndiff  36045  ifscgr  36062  seglecgr12im  36128  atlatle  39338  cvlcvr1  39357  atbtwn  39465  3dimlem3  39480  3dimlem3OLDN  39481  4atlem3  39615  4atlem11  39628  4atlem12  39631  2lplnj  39639  paddasslem4  39842  paddasslem10  39848  pmodlem1  39865  llnexchb2lem  39887  pclfinclN  39969  arglem1N  40209  cdlemd4  40220  cdlemd  40226  cdleme16  40304  cdleme20  40343  cdleme21k  40357  cdleme22cN  40361  cdleme27N  40388  cdleme28c  40391  cdleme29ex  40393  cdleme32fva  40456  cdleme40n  40487  cdlemg15a  40674  cdlemg15  40675  cdlemg16ALTN  40677  cdlemg16z  40678  cdlemg20  40704  cdlemg22  40706  cdlemg29  40724  cdlemg38  40734  cdlemk56  40990  dihord2pre  41244  ismnu  44285  uzwo4  45077  fourierdlem77  46212