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 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  pythagtriplem4  16759  tsmsxp  24111  nolt02o  27675  nogt01o  27676  cofslts  27926  brbtwn2  28990  ax5seg  29023  3vfriswmgr  30365  br8  35969  btwndiff  36240  ifscgr  36257  seglecgr12im  36323  lkrshp  39478  cvlcvr1  39712  atbtwn  39819  3dimlem3  39834  3dimlem3OLDN  39835  1cvratex  39846  llnmlplnN  39912  4atlem3  39969  4atlem3a  39970  4atlem11  39982  4atlem12  39985  lnatexN  40152  cdlemb  40167  paddasslem4  40196  paddasslem10  40202  pmodlem1  40219  llnexchb2lem  40241  llnexchb2  40242  arglem1N  40563  cdlemd4  40574  cdlemd9  40579  cdlemd  40580  cdleme16  40658  cdleme20  40697  cdleme21i  40708  cdleme21k  40711  cdleme27N  40742  cdleme28c  40745  cdlemefrs29bpre0  40769  cdlemefrs29clN  40772  cdlemefrs32fva  40773  cdleme41sn3a  40806  cdleme32fva  40810  cdleme40n  40841  cdlemg12e  41020  cdlemg15a  41028  cdlemg15  41029  cdlemg16ALTN  41031  cdlemg16z  41032  cdlemg20  41058  cdlemg22  41060  cdlemg29  41078  cdlemg38  41088  cdlemk33N  41282  cdlemk56  41344  dihord11b  41595  dihord2pre  41598  dihord4  41631  ismnu  44614  fourierdlem77  46538