Theorem simpl12 1250

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl12	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl12

Step	Hyp	Ref	Expression
1		simpl2 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl1 1186	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

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

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 1088

This theorem is referenced by:  pythagtriplem4  16728  pmatcollpw1lem1  22687  pmatcollpw1  22689  mp2pm2mplem2  22720  nolt02o  27632  nogt01o  27633  brbtwn2  28881  ax5seg  28914  3vfriswmgr  30253  br8  35788  ifscgr  36077  seglecgr12im  36143  lkrshp  39143  atlatle  39358  cvlcvr1  39377  atbtwn  39484  3dimlem3  39499  3dimlem3OLDN  39500  1cvratex  39511  llnmlplnN  39577  4atlem3  39634  4atlem3a  39635  4atlem11  39647  4atlem12  39650  cdlemb  39832  paddasslem4  39861  paddasslem10  39867  pmodlem1  39884  llnexchb2lem  39906  arglem1N  40228  cdlemd4  40239  cdlemd  40245  cdleme16  40323  cdleme20  40362  cdleme21k  40376  cdleme22cN  40380  cdleme27N  40407  cdleme28c  40410  cdleme29ex  40412  cdleme32fva  40475  cdleme40n  40506  cdlemg15a  40693  cdlemg15  40694  cdlemg16ALTN  40696  cdlemg16z  40697  cdlemg20  40723  cdlemg22  40725  cdlemg29  40743  cdlemg38  40753  cdlemk33N  40947  cdlemk56  41009  fourierdlem77  46220