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  16839  tsmsxp  24093  nolt02o  27659  nogt01o  27660  cofsslt  27878  brbtwn2  28884  ax5seg  28917  3vfriswmgr  30259  br8  35773  btwndiff  36045  ifscgr  36062  seglecgr12im  36128  lkrshp  39123  cvlcvr1  39357  atbtwn  39465  3dimlem3  39480  3dimlem3OLDN  39481  1cvratex  39492  llnmlplnN  39558  4atlem3  39615  4atlem3a  39616  4atlem11  39628  4atlem12  39631  lnatexN  39798  cdlemb  39813  paddasslem4  39842  paddasslem10  39848  pmodlem1  39865  llnexchb2lem  39887  llnexchb2  39888  arglem1N  40209  cdlemd4  40220  cdlemd9  40225  cdlemd  40226  cdleme16  40304  cdleme20  40343  cdleme21i  40354  cdleme21k  40357  cdleme27N  40388  cdleme28c  40391  cdlemefrs29bpre0  40415  cdlemefrs29clN  40418  cdlemefrs32fva  40419  cdleme41sn3a  40452  cdleme32fva  40456  cdleme40n  40487  cdlemg12e  40666  cdlemg15a  40674  cdlemg15  40675  cdlemg16ALTN  40677  cdlemg16z  40678  cdlemg20  40704  cdlemg22  40706  cdlemg29  40724  cdlemg38  40734  cdlemk33N  40928  cdlemk56  40990  dihord11b  41241  dihord2pre  41244  dihord4  41277  ismnu  44285  fourierdlem77  46212