Theorem simpl11 1244

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pythagtriplem4  16158  tsmsxp  22765  brbtwn2  26693  ax5seg  26726  3vfriswmgr  28059  br8  32994  nolt02o  33201  btwndiff  33490  ifscgr  33507  seglecgr12im  33573  lkrshp  36243  cvlcvr1  36477  atbtwn  36584  3dimlem3  36599  3dimlem3OLDN  36600  1cvratex  36611  llnmlplnN  36677  4atlem3  36734  4atlem3a  36735  4atlem11  36747  4atlem12  36750  lnatexN  36917  cdlemb  36932  paddasslem4  36961  paddasslem10  36967  pmodlem1  36984  llnexchb2lem  37006  llnexchb2  37007  arglem1N  37328  cdlemd4  37339  cdlemd9  37344  cdlemd  37345  cdleme16  37423  cdleme20  37462  cdleme21i  37473  cdleme21k  37476  cdleme27N  37507  cdleme28c  37510  cdlemefrs29bpre0  37534  cdlemefrs29clN  37537  cdlemefrs32fva  37538  cdleme41sn3a  37571  cdleme32fva  37575  cdleme40n  37606  cdlemg12e  37785  cdlemg15a  37793  cdlemg15  37794  cdlemg16ALTN  37796  cdlemg16z  37797  cdlemg20  37823  cdlemg22  37825  cdlemg29  37843  cdlemg38  37853  cdlemk33N  38047  cdlemk56  38109  dihord11b  38360  dihord2pre  38363  dihord4  38396  ismnu  40604  fourierdlem77  42475