Theorem simpl13 1252

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 1195	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl1 1187	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pythagtriplem4  16790  mply1topmatcl  22770  nolt02o  27659  nogt01o  27660  cofslts  27910  coinitslts  27911  brbtwn2  28974  ax5seg  29007  br8  35938  btwndiff  36209  ifscgr  36226  seglecgr12im  36292  atlatle  39766  cvlcvr1  39785  atbtwn  39892  3dimlem3  39907  3dimlem3OLDN  39908  4atlem3  40042  4atlem11  40055  4atlem12  40058  2lplnj  40066  paddasslem4  40269  paddasslem10  40275  pmodlem1  40292  llnexchb2lem  40314  pclfinclN  40396  arglem1N  40636  cdlemd4  40647  cdlemd  40653  cdleme16  40731  cdleme20  40770  cdleme21k  40784  cdleme22cN  40788  cdleme27N  40815  cdleme28c  40818  cdleme29ex  40820  cdleme32fva  40883  cdleme40n  40914  cdlemg15a  41101  cdlemg15  41102  cdlemg16ALTN  41104  cdlemg16z  41105  cdlemg20  41131  cdlemg22  41133  cdlemg29  41151  cdlemg38  41161  cdlemk56  41417  dihord2pre  41671  ismnu  44688  uzwo4  45484  fourierdlem77  46611