Theorem simpl11 1247

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 1190	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1184	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  16853  tsmsxp  24179  nolt02o  27755  nogt01o  27756  cofsslt  27967  brbtwn2  28935  ax5seg  28968  3vfriswmgr  30307  br8  35736  btwndiff  36009  ifscgr  36026  seglecgr12im  36092  lkrshp  39087  cvlcvr1  39321  atbtwn  39429  3dimlem3  39444  3dimlem3OLDN  39445  1cvratex  39456  llnmlplnN  39522  4atlem3  39579  4atlem3a  39580  4atlem11  39592  4atlem12  39595  lnatexN  39762  cdlemb  39777  paddasslem4  39806  paddasslem10  39812  pmodlem1  39829  llnexchb2lem  39851  llnexchb2  39852  arglem1N  40173  cdlemd4  40184  cdlemd9  40189  cdlemd  40190  cdleme16  40268  cdleme20  40307  cdleme21i  40318  cdleme21k  40321  cdleme27N  40352  cdleme28c  40355  cdlemefrs29bpre0  40379  cdlemefrs29clN  40382  cdlemefrs32fva  40383  cdleme41sn3a  40416  cdleme32fva  40420  cdleme40n  40451  cdlemg12e  40630  cdlemg15a  40638  cdlemg15  40639  cdlemg16ALTN  40641  cdlemg16z  40642  cdlemg20  40668  cdlemg22  40670  cdlemg29  40688  cdlemg38  40698  cdlemk33N  40892  cdlemk56  40954  dihord11b  41205  dihord2pre  41208  dihord4  41241  ismnu  44257  fourierdlem77  46139