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 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  pythagtriplem4  16752  tsmsxp  23659  nolt02o  27198  nogt01o  27199  cofsslt  27405  brbtwn2  28163  ax5seg  28196  3vfriswmgr  29531  br8  34726  btwndiff  34999  ifscgr  35016  seglecgr12im  35082  lkrshp  37975  cvlcvr1  38209  atbtwn  38317  3dimlem3  38332  3dimlem3OLDN  38333  1cvratex  38344  llnmlplnN  38410  4atlem3  38467  4atlem3a  38468  4atlem11  38480  4atlem12  38483  lnatexN  38650  cdlemb  38665  paddasslem4  38694  paddasslem10  38700  pmodlem1  38717  llnexchb2lem  38739  llnexchb2  38740  arglem1N  39061  cdlemd4  39072  cdlemd9  39077  cdlemd  39078  cdleme16  39156  cdleme20  39195  cdleme21i  39206  cdleme21k  39209  cdleme27N  39240  cdleme28c  39243  cdlemefrs29bpre0  39267  cdlemefrs29clN  39270  cdlemefrs32fva  39271  cdleme41sn3a  39304  cdleme32fva  39308  cdleme40n  39339  cdlemg12e  39518  cdlemg15a  39526  cdlemg15  39527  cdlemg16ALTN  39529  cdlemg16z  39530  cdlemg20  39556  cdlemg22  39558  cdlemg29  39576  cdlemg38  39586  cdlemk33N  39780  cdlemk56  39842  dihord11b  40093  dihord2pre  40096  dihord4  40129  ismnu  43020  fourierdlem77  44899