Theorem simpl11 1250

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 1193	. 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  tsmsxp  24120  nolt02o  27659  nogt01o  27660  cofslts  27910  brbtwn2  28974  ax5seg  29007  3vfriswmgr  30348  br8  35938  btwndiff  36209  ifscgr  36226  seglecgr12im  36292  lkrshp  39551  cvlcvr1  39785  atbtwn  39892  3dimlem3  39907  3dimlem3OLDN  39908  1cvratex  39919  llnmlplnN  39985  4atlem3  40042  4atlem3a  40043  4atlem11  40055  4atlem12  40058  lnatexN  40225  cdlemb  40240  paddasslem4  40269  paddasslem10  40275  pmodlem1  40292  llnexchb2lem  40314  llnexchb2  40315  arglem1N  40636  cdlemd4  40647  cdlemd9  40652  cdlemd  40653  cdleme16  40731  cdleme20  40770  cdleme21i  40781  cdleme21k  40784  cdleme27N  40815  cdleme28c  40818  cdlemefrs29bpre0  40842  cdlemefrs29clN  40845  cdlemefrs32fva  40846  cdleme41sn3a  40879  cdleme32fva  40883  cdleme40n  40914  cdlemg12e  41093  cdlemg15a  41101  cdlemg15  41102  cdlemg16ALTN  41104  cdlemg16z  41105  cdlemg20  41131  cdlemg22  41133  cdlemg29  41151  cdlemg38  41161  cdlemk33N  41355  cdlemk56  41417  dihord11b  41668  dihord2pre  41671  dihord4  41704  ismnu  44688  fourierdlem77  46611