Theorem simpl11 1261

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  pythagtriplem4  16845  tsmsxp  24202  nolt02o  27746  nogt01o  27747  cofslts  27998  brbtwn2  29062  ax5seg  29095  3vfriswmgr  30436  br8  36066  btwndiff  36337  ifscgr  36354  seglecgr12im  36420  lkrshp  39689  cvlcvr1  39923  atbtwn  40030  3dimlem3  40045  3dimlem3OLDN  40046  1cvratex  40057  llnmlplnN  40123  4atlem3  40180  4atlem3a  40181  4atlem11  40193  4atlem12  40196  lnatexN  40363  cdlemb  40378  paddasslem4  40407  paddasslem10  40413  pmodlem1  40430  llnexchb2lem  40452  llnexchb2  40453  arglem1N  40774  cdlemd4  40785  cdlemd9  40790  cdlemd  40791  cdleme16  40869  cdleme20  40908  cdleme21i  40919  cdleme21k  40922  cdleme27N  40953  cdleme28c  40956  cdlemefrs29bpre0  40980  cdlemefrs29clN  40983  cdlemefrs32fva  40984  cdleme41sn3a  41017  cdleme32fva  41021  cdleme40n  41052  cdlemg12e  41231  cdlemg15a  41239  cdlemg15  41240  cdlemg16ALTN  41242  cdlemg16z  41243  cdlemg20  41269  cdlemg22  41271  cdlemg29  41289  cdlemg38  41299  cdlemk33N  41493  cdlemk56  41555  dihord11b  41806  dihord2pre  41809  dihord4  41842  ismnu  44797  fourierdlem77  46717