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  16790  tsmsxp  24042  nolt02o  27607  nogt01o  27608  cofsslt  27826  brbtwn2  28832  ax5seg  28865  3vfriswmgr  30207  br8  35743  btwndiff  36015  ifscgr  36032  seglecgr12im  36098  lkrshp  39098  cvlcvr1  39332  atbtwn  39440  3dimlem3  39455  3dimlem3OLDN  39456  1cvratex  39467  llnmlplnN  39533  4atlem3  39590  4atlem3a  39591  4atlem11  39603  4atlem12  39606  lnatexN  39773  cdlemb  39788  paddasslem4  39817  paddasslem10  39823  pmodlem1  39840  llnexchb2lem  39862  llnexchb2  39863  arglem1N  40184  cdlemd4  40195  cdlemd9  40200  cdlemd  40201  cdleme16  40279  cdleme20  40318  cdleme21i  40329  cdleme21k  40332  cdleme27N  40363  cdleme28c  40366  cdlemefrs29bpre0  40390  cdlemefrs29clN  40393  cdlemefrs32fva  40394  cdleme41sn3a  40427  cdleme32fva  40431  cdleme40n  40462  cdlemg12e  40641  cdlemg15a  40649  cdlemg15  40650  cdlemg16ALTN  40652  cdlemg16z  40653  cdlemg20  40679  cdlemg22  40681  cdlemg29  40699  cdlemg38  40709  cdlemk33N  40903  cdlemk56  40965  dihord11b  41216  dihord2pre  41219  dihord4  41252  ismnu  44250  fourierdlem77  46181