Theorem simpl11 1249

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl1 1186	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  16749  tsmsxp  24058  nolt02o  27623  nogt01o  27624  cofsslt  27849  brbtwn2  28868  ax5seg  28901  3vfriswmgr  30240  br8  35728  btwndiff  36000  ifscgr  36017  seglecgr12im  36083  lkrshp  39083  cvlcvr1  39317  atbtwn  39425  3dimlem3  39440  3dimlem3OLDN  39441  1cvratex  39452  llnmlplnN  39518  4atlem3  39575  4atlem3a  39576  4atlem11  39588  4atlem12  39591  lnatexN  39758  cdlemb  39773  paddasslem4  39802  paddasslem10  39808  pmodlem1  39825  llnexchb2lem  39847  llnexchb2  39848  arglem1N  40169  cdlemd4  40180  cdlemd9  40185  cdlemd  40186  cdleme16  40264  cdleme20  40303  cdleme21i  40314  cdleme21k  40317  cdleme27N  40348  cdleme28c  40351  cdlemefrs29bpre0  40375  cdlemefrs29clN  40378  cdlemefrs32fva  40379  cdleme41sn3a  40412  cdleme32fva  40416  cdleme40n  40447  cdlemg12e  40626  cdlemg15a  40634  cdlemg15  40635  cdlemg16ALTN  40637  cdlemg16z  40638  cdlemg20  40664  cdlemg22  40666  cdlemg29  40684  cdlemg38  40694  cdlemk33N  40888  cdlemk56  40950  dihord11b  41201  dihord2pre  41204  dihord4  41237  ismnu  44234  fourierdlem77  46165