Theorem simpl11 1249

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 1192	. 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  16733  tsmsxp  24071  nolt02o  27635  nogt01o  27636  cofsslt  27863  brbtwn2  28885  ax5seg  28918  3vfriswmgr  30260  br8  35821  btwndiff  36092  ifscgr  36109  seglecgr12im  36175  lkrshp  39225  cvlcvr1  39459  atbtwn  39566  3dimlem3  39581  3dimlem3OLDN  39582  1cvratex  39593  llnmlplnN  39659  4atlem3  39716  4atlem3a  39717  4atlem11  39729  4atlem12  39732  lnatexN  39899  cdlemb  39914  paddasslem4  39943  paddasslem10  39949  pmodlem1  39966  llnexchb2lem  39988  llnexchb2  39989  arglem1N  40310  cdlemd4  40321  cdlemd9  40326  cdlemd  40327  cdleme16  40405  cdleme20  40444  cdleme21i  40455  cdleme21k  40458  cdleme27N  40489  cdleme28c  40492  cdlemefrs29bpre0  40516  cdlemefrs29clN  40519  cdlemefrs32fva  40520  cdleme41sn3a  40553  cdleme32fva  40557  cdleme40n  40588  cdlemg12e  40767  cdlemg15a  40775  cdlemg15  40776  cdlemg16ALTN  40778  cdlemg16z  40779  cdlemg20  40805  cdlemg22  40807  cdlemg29  40825  cdlemg38  40835  cdlemk33N  41029  cdlemk56  41091  dihord11b  41342  dihord2pre  41345  dihord4  41378  ismnu  44379  fourierdlem77  46306