Theorem simpl11 1248

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  pythagtriplem4  16756  tsmsxp  23879  nolt02o  27422  nogt01o  27423  cofsslt  27631  brbtwn2  28418  ax5seg  28451  3vfriswmgr  29786  br8  35018  btwndiff  35291  ifscgr  35308  seglecgr12im  35374  lkrshp  38278  cvlcvr1  38512  atbtwn  38620  3dimlem3  38635  3dimlem3OLDN  38636  1cvratex  38647  llnmlplnN  38713  4atlem3  38770  4atlem3a  38771  4atlem11  38783  4atlem12  38786  lnatexN  38953  cdlemb  38968  paddasslem4  38997  paddasslem10  39003  pmodlem1  39020  llnexchb2lem  39042  llnexchb2  39043  arglem1N  39364  cdlemd4  39375  cdlemd9  39380  cdlemd  39381  cdleme16  39459  cdleme20  39498  cdleme21i  39509  cdleme21k  39512  cdleme27N  39543  cdleme28c  39546  cdlemefrs29bpre0  39570  cdlemefrs29clN  39573  cdlemefrs32fva  39574  cdleme41sn3a  39607  cdleme32fva  39611  cdleme40n  39642  cdlemg12e  39821  cdlemg15a  39829  cdlemg15  39830  cdlemg16ALTN  39832  cdlemg16z  39833  cdlemg20  39859  cdlemg22  39861  cdlemg29  39879  cdlemg38  39889  cdlemk33N  40083  cdlemk56  40145  dihord11b  40396  dihord2pre  40399  dihord4  40432  ismnu  43322  fourierdlem77  45198