Theorem simpl11 1267

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

Assertion

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

Proof of Theorem simpl11

Step	Hyp	Ref	Expression
1		simpl1 1210	. 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  tsmsxp  24293  nolt02o  27840  nogt01o  27841  cofslts  28092  brbtwn2  29236  ax5seg  29269  3vfriswmgr  30610  br8  36229  btwndiff  36500  ifscgr  36517  seglecgr12im  36583  lkrshp  39860  cvlcvr1  40094  atbtwn  40201  3dimlem3  40216  3dimlem3OLDN  40217  1cvratex  40228  llnmlplnN  40294  4atlem3  40351  4atlem3a  40352  4atlem11  40364  4atlem12  40367  lnatexN  40534  cdlemb  40549  paddasslem4  40578  paddasslem10  40584  pmodlem1  40601  llnexchb2lem  40623  llnexchb2  40624  arglem1N  40945  cdlemd4  40956  cdlemd9  40961  cdlemd  40962  cdleme16  41040  cdleme20  41079  cdleme21i  41090  cdleme21k  41093  cdleme27N  41124  cdleme28c  41127  cdlemefrs29bpre0  41151  cdlemefrs29clN  41154  cdlemefrs32fva  41155  cdleme41sn3a  41188  cdleme32fva  41192  cdleme40n  41223  cdlemg12e  41402  cdlemg15a  41410  cdlemg15  41411  cdlemg16ALTN  41413  cdlemg16z  41414  cdlemg20  41440  cdlemg22  41442  cdlemg29  41460  cdlemg38  41470  cdlemk33N  41664  cdlemk56  41726  dihord11b  41977  dihord2pre  41980  dihord4  42013  ismnu  44954  fourierdlem77  46880