Theorem simpl11 1247

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16518  tsmsxp  23304  brbtwn2  27271  ax5seg  27304  3vfriswmgr  28638  br8  33719  poxp3  33792  nolt02o  33894  nogt01o  33895  cofsslt  34084  btwndiff  34325  ifscgr  34342  seglecgr12im  34408  lkrshp  37115  cvlcvr1  37349  atbtwn  37456  3dimlem3  37471  3dimlem3OLDN  37472  1cvratex  37483  llnmlplnN  37549  4atlem3  37606  4atlem3a  37607  4atlem11  37619  4atlem12  37622  lnatexN  37789  cdlemb  37804  paddasslem4  37833  paddasslem10  37839  pmodlem1  37856  llnexchb2lem  37878  llnexchb2  37879  arglem1N  38200  cdlemd4  38211  cdlemd9  38216  cdlemd  38217  cdleme16  38295  cdleme20  38334  cdleme21i  38345  cdleme21k  38348  cdleme27N  38379  cdleme28c  38382  cdlemefrs29bpre0  38406  cdlemefrs29clN  38409  cdlemefrs32fva  38410  cdleme41sn3a  38443  cdleme32fva  38447  cdleme40n  38478  cdlemg12e  38657  cdlemg15a  38665  cdlemg15  38666  cdlemg16ALTN  38668  cdlemg16z  38669  cdlemg20  38695  cdlemg22  38697  cdlemg29  38715  cdlemg38  38725  cdlemk33N  38919  cdlemk56  38981  dihord11b  39232  dihord2pre  39235  dihord4  39268  ismnu  41849  fourierdlem77  43695