Theorem simpl11 1255

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  pythagtriplem4  16788  tsmsxp  24145  nolt02o  27684  nogt01o  27685  cofslts  27935  brbtwn2  28999  ax5seg  29032  3vfriswmgr  30373  br8  35991  btwndiff  36262  ifscgr  36279  seglecgr12im  36345  lkrshp  39604  cvlcvr1  39838  atbtwn  39945  3dimlem3  39960  3dimlem3OLDN  39961  1cvratex  39972  llnmlplnN  40038  4atlem3  40095  4atlem3a  40096  4atlem11  40108  4atlem12  40111  lnatexN  40278  cdlemb  40293  paddasslem4  40322  paddasslem10  40328  pmodlem1  40345  llnexchb2lem  40367  llnexchb2  40368  arglem1N  40689  cdlemd4  40700  cdlemd9  40705  cdlemd  40706  cdleme16  40784  cdleme20  40823  cdleme21i  40834  cdleme21k  40837  cdleme27N  40868  cdleme28c  40871  cdlemefrs29bpre0  40895  cdlemefrs29clN  40898  cdlemefrs32fva  40899  cdleme41sn3a  40932  cdleme32fva  40936  cdleme40n  40967  cdlemg12e  41146  cdlemg15a  41154  cdlemg15  41155  cdlemg16ALTN  41157  cdlemg16z  41158  cdlemg20  41184  cdlemg22  41186  cdlemg29  41204  cdlemg38  41214  cdlemk33N  41408  cdlemk56  41470  dihord11b  41721  dihord2pre  41724  dihord4  41757  ismnu  44712  fourierdlem77  46633