Theorem simpl11 1265

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pythagtriplem4  16867  tsmsxp  24269  nolt02o  27813  nogt01o  27814  cofslts  28065  brbtwn2  29160  ax5seg  29193  3vfriswmgr  30534  br8  36114  btwndiff  36385  ifscgr  36402  seglecgr12im  36468  lkrshp  39736  cvlcvr1  39970  atbtwn  40077  3dimlem3  40092  3dimlem3OLDN  40093  1cvratex  40104  llnmlplnN  40170  4atlem3  40227  4atlem3a  40228  4atlem11  40240  4atlem12  40243  lnatexN  40410  cdlemb  40425  paddasslem4  40454  paddasslem10  40460  pmodlem1  40477  llnexchb2lem  40499  llnexchb2  40500  arglem1N  40821  cdlemd4  40832  cdlemd9  40837  cdlemd  40838  cdleme16  40916  cdleme20  40955  cdleme21i  40966  cdleme21k  40969  cdleme27N  41000  cdleme28c  41003  cdlemefrs29bpre0  41027  cdlemefrs29clN  41030  cdlemefrs32fva  41031  cdleme41sn3a  41064  cdleme32fva  41068  cdleme40n  41099  cdlemg12e  41278  cdlemg15a  41286  cdlemg15  41287  cdlemg16ALTN  41289  cdlemg16z  41290  cdlemg20  41316  cdlemg22  41318  cdlemg29  41336  cdlemg38  41346  cdlemk33N  41540  cdlemk56  41602  dihord11b  41853  dihord2pre  41856  dihord4  41889  ismnu  44830  fourierdlem77  46756