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  16839  pmatcollpw1lem1  22712  pmatcollpw1  22714  mp2pm2mplem2  22745  nolt02o  27659  nogt01o  27660  brbtwn2  28884  ax5seg  28917  3vfriswmgr  30259  br8  35773  ifscgr  36062  seglecgr12im  36128  lkrshp  39123  atlatle  39338  cvlcvr1  39357  atbtwn  39465  3dimlem3  39480  3dimlem3OLDN  39481  1cvratex  39492  llnmlplnN  39558  4atlem3  39615  4atlem3a  39616  4atlem11  39628  4atlem12  39631  cdlemb  39813  paddasslem4  39842  paddasslem10  39848  pmodlem1  39865  llnexchb2lem  39887  arglem1N  40209  cdlemd4  40220  cdlemd  40226  cdleme16  40304  cdleme20  40343  cdleme21k  40357  cdleme22cN  40361  cdleme27N  40388  cdleme28c  40391  cdleme29ex  40393  cdleme32fva  40456  cdleme40n  40487  cdlemg15a  40674  cdlemg15  40675  cdlemg16ALTN  40677  cdlemg16z  40678  cdlemg20  40704  cdlemg22  40706  cdlemg29  40724  cdlemg38  40734  cdlemk33N  40928  cdlemk56  40990  fourierdlem77  46212