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  16781  tsmsxp  24130  nolt02o  27673  nogt01o  27674  cofslts  27924  brbtwn2  28988  ax5seg  29021  3vfriswmgr  30363  br8  35954  btwndiff  36225  ifscgr  36242  seglecgr12im  36308  lkrshp  39565  cvlcvr1  39799  atbtwn  39906  3dimlem3  39921  3dimlem3OLDN  39922  1cvratex  39933  llnmlplnN  39999  4atlem3  40056  4atlem3a  40057  4atlem11  40069  4atlem12  40072  lnatexN  40239  cdlemb  40254  paddasslem4  40283  paddasslem10  40289  pmodlem1  40306  llnexchb2lem  40328  llnexchb2  40329  arglem1N  40650  cdlemd4  40661  cdlemd9  40666  cdlemd  40667  cdleme16  40745  cdleme20  40784  cdleme21i  40795  cdleme21k  40798  cdleme27N  40829  cdleme28c  40832  cdlemefrs29bpre0  40856  cdlemefrs29clN  40859  cdlemefrs32fva  40860  cdleme41sn3a  40893  cdleme32fva  40897  cdleme40n  40928  cdlemg12e  41107  cdlemg15a  41115  cdlemg15  41116  cdlemg16ALTN  41118  cdlemg16z  41119  cdlemg20  41145  cdlemg22  41147  cdlemg29  41165  cdlemg38  41175  cdlemk33N  41369  cdlemk56  41431  dihord11b  41682  dihord2pre  41685  dihord4  41718  ismnu  44706  fourierdlem77  46629