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  16728  tsmsxp  24068  nolt02o  27632  nogt01o  27633  cofsslt  27860  brbtwn2  28881  ax5seg  28914  3vfriswmgr  30253  br8  35788  btwndiff  36060  ifscgr  36077  seglecgr12im  36143  lkrshp  39143  cvlcvr1  39377  atbtwn  39484  3dimlem3  39499  3dimlem3OLDN  39500  1cvratex  39511  llnmlplnN  39577  4atlem3  39634  4atlem3a  39635  4atlem11  39647  4atlem12  39650  lnatexN  39817  cdlemb  39832  paddasslem4  39861  paddasslem10  39867  pmodlem1  39884  llnexchb2lem  39906  llnexchb2  39907  arglem1N  40228  cdlemd4  40239  cdlemd9  40244  cdlemd  40245  cdleme16  40323  cdleme20  40362  cdleme21i  40373  cdleme21k  40376  cdleme27N  40407  cdleme28c  40410  cdlemefrs29bpre0  40434  cdlemefrs29clN  40437  cdlemefrs32fva  40438  cdleme41sn3a  40471  cdleme32fva  40475  cdleme40n  40506  cdlemg12e  40685  cdlemg15a  40693  cdlemg15  40694  cdlemg16ALTN  40696  cdlemg16z  40697  cdlemg20  40723  cdlemg22  40725  cdlemg29  40743  cdlemg38  40753  cdlemk33N  40947  cdlemk56  41009  dihord11b  41260  dihord2pre  41263  dihord4  41296  ismnu  44293  fourierdlem77  46220