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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16917  tsmsxp  24387  nolt02o  27939  nogt01o  27940  cofslts  28191  brbtwn2  29370  ax5seg  29403  3vfriswmgr  30766  br8  36343  btwndiff  36615  ifscgr  36632  seglecgr12im  36698  lkrshp  39986  cvlcvr1  40220  atbtwn  40327  3dimlem3  40342  3dimlem3OLDN  40343  1cvratex  40354  llnmlplnN  40420  4atlem3  40477  4atlem3a  40478  4atlem11  40490  4atlem12  40493  lnatexN  40660  cdlemb  40675  paddasslem4  40704  paddasslem10  40710  pmodlem1  40727  llnexchb2lem  40749  llnexchb2  40750  arglem1N  41071  cdlemd4  41082  cdlemd9  41087  cdlemd  41088  cdleme16  41166  cdleme20  41205  cdleme21i  41216  cdleme21k  41219  cdleme27N  41250  cdleme28c  41253  cdlemefrs29bpre0  41277  cdlemefrs29clN  41280  cdlemefrs32fva  41281  cdleme41sn3a  41314  cdleme32fva  41318  cdleme40n  41349  cdlemg12e  41528  cdlemg15a  41536  cdlemg15  41537  cdlemg16ALTN  41539  cdlemg16z  41540  cdlemg20  41566  cdlemg22  41568  cdlemg29  41586  cdlemg38  41596  cdlemk33N  41790  cdlemk56  41852  dihord11b  42103  dihord2pre  42106  dihord4  42139  ismnu  45093  fourierdlem77  47019