Theorem simpl13 1269

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 210  df-an 401  df-3an 1105

This theorem is referenced by:  pythagtriplem4  16880  mply1topmatcl  22943  nolt02o  27840  nogt01o  27841  cofslts  28092  coinitslts  28093  brbtwn2  29236  ax5seg  29269  br8  36229  btwndiff  36500  ifscgr  36517  seglecgr12im  36583  atlatle  40075  cvlcvr1  40094  atbtwn  40201  3dimlem3  40216  3dimlem3OLDN  40217  4atlem3  40351  4atlem11  40364  4atlem12  40367  2lplnj  40375  paddasslem4  40578  paddasslem10  40584  pmodlem1  40601  llnexchb2lem  40623  pclfinclN  40705  arglem1N  40945  cdlemd4  40956  cdlemd  40962  cdleme16  41040  cdleme20  41079  cdleme21k  41093  cdleme22cN  41097  cdleme27N  41124  cdleme28c  41127  cdleme29ex  41129  cdleme32fva  41192  cdleme40n  41223  cdlemg15a  41410  cdlemg15  41411  cdlemg16ALTN  41413  cdlemg16z  41414  cdlemg20  41440  cdlemg22  41442  cdlemg29  41460  cdlemg38  41470  cdlemk56  41726  dihord2pre  41980  ismnu  44954  uzwo4  45756  fourierdlem77  46880