Theorem simpl11 1250

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 400  df-3an 1091

This theorem is referenced by:  pythagtriplem4  16335  tsmsxp  23006  brbtwn2  26950  ax5seg  26983  3vfriswmgr  28315  br8  33393  poxp3  33476  nolt02o  33584  nogt01o  33585  cofsslt  33774  btwndiff  34015  ifscgr  34032  seglecgr12im  34098  lkrshp  36805  cvlcvr1  37039  atbtwn  37146  3dimlem3  37161  3dimlem3OLDN  37162  1cvratex  37173  llnmlplnN  37239  4atlem3  37296  4atlem3a  37297  4atlem11  37309  4atlem12  37312  lnatexN  37479  cdlemb  37494  paddasslem4  37523  paddasslem10  37529  pmodlem1  37546  llnexchb2lem  37568  llnexchb2  37569  arglem1N  37890  cdlemd4  37901  cdlemd9  37906  cdlemd  37907  cdleme16  37985  cdleme20  38024  cdleme21i  38035  cdleme21k  38038  cdleme27N  38069  cdleme28c  38072  cdlemefrs29bpre0  38096  cdlemefrs29clN  38099  cdlemefrs32fva  38100  cdleme41sn3a  38133  cdleme32fva  38137  cdleme40n  38168  cdlemg12e  38347  cdlemg15a  38355  cdlemg15  38356  cdlemg16ALTN  38358  cdlemg16z  38359  cdlemg20  38385  cdlemg22  38387  cdlemg29  38405  cdlemg38  38415  cdlemk33N  38609  cdlemk56  38671  dihord11b  38922  dihord2pre  38925  dihord4  38958  ismnu  41493  fourierdlem77  43342