Theorem simpl11 1267

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  17029  tsmsxp  24507  nolt02o  28085  nogt01o  28086  cofslts  28337  brbtwn2  29516  ax5seg  29549  3vfriswmgr  30912  br8  36712  btwndiff  36983  ifscgr  37000  seglecgr12im  37066  lkrshp  40365  cvlcvr1  40599  atbtwn  40706  3dimlem3  40721  3dimlem3OLDN  40722  1cvratex  40733  llnmlplnN  40799  4atlem3  40856  4atlem3a  40857  4atlem11  40869  4atlem12  40872  lnatexN  41039  cdlemb  41054  paddasslem4  41083  paddasslem10  41089  pmodlem1  41106  llnexchb2lem  41128  llnexchb2  41129  arglem1N  41450  cdlemd4  41461  cdlemd9  41466  cdlemd  41467  cdleme16  41545  cdleme20  41584  cdleme21i  41595  cdleme21k  41598  cdleme27N  41629  cdleme28c  41632  cdlemefrs29bpre0  41656  cdlemefrs29clN  41659  cdlemefrs32fva  41660  cdleme41sn3a  41693  cdleme32fva  41697  cdleme40n  41728  cdlemg12e  41907  cdlemg15a  41915  cdlemg15  41916  cdlemg16ALTN  41918  cdlemg16z  41919  cdlemg20  41945  cdlemg22  41947  cdlemg29  41965  cdlemg38  41975  cdlemk33N  42169  cdlemk56  42231  dihord11b  42482  dihord2pre  42485  dihord4  42518  ismnu  45448  fourierdlem77  47408