Theorem simpl11 1246

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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

This theorem is referenced by:  pythagtriplem4  16448  tsmsxp  23214  brbtwn2  27176  ax5seg  27209  3vfriswmgr  28543  br8  33629  poxp3  33723  nolt02o  33825  nogt01o  33826  cofsslt  34015  btwndiff  34256  ifscgr  34273  seglecgr12im  34339  lkrshp  37046  cvlcvr1  37280  atbtwn  37387  3dimlem3  37402  3dimlem3OLDN  37403  1cvratex  37414  llnmlplnN  37480  4atlem3  37537  4atlem3a  37538  4atlem11  37550  4atlem12  37553  lnatexN  37720  cdlemb  37735  paddasslem4  37764  paddasslem10  37770  pmodlem1  37787  llnexchb2lem  37809  llnexchb2  37810  arglem1N  38131  cdlemd4  38142  cdlemd9  38147  cdlemd  38148  cdleme16  38226  cdleme20  38265  cdleme21i  38276  cdleme21k  38279  cdleme27N  38310  cdleme28c  38313  cdlemefrs29bpre0  38337  cdlemefrs29clN  38340  cdlemefrs32fva  38341  cdleme41sn3a  38374  cdleme32fva  38378  cdleme40n  38409  cdlemg12e  38588  cdlemg15a  38596  cdlemg15  38597  cdlemg16ALTN  38599  cdlemg16z  38600  cdlemg20  38626  cdlemg22  38628  cdlemg29  38646  cdlemg38  38656  cdlemk33N  38850  cdlemk56  38912  dihord11b  39163  dihord2pre  39166  dihord4  39199  ismnu  41768  fourierdlem77  43614