Theorem simpl12 1247

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 1190	. 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  16782  pmatcollpw1lem1  22670  pmatcollpw1  22672  mp2pm2mplem2  22703  nolt02o  27622  nogt01o  27623  brbtwn2  28710  ax5seg  28743  3vfriswmgr  30082  br8  35345  ifscgr  35635  seglecgr12im  35701  lkrshp  38572  atlatle  38787  cvlcvr1  38806  atbtwn  38914  3dimlem3  38929  3dimlem3OLDN  38930  1cvratex  38941  llnmlplnN  39007  4atlem3  39064  4atlem3a  39065  4atlem11  39077  4atlem12  39080  cdlemb  39262  paddasslem4  39291  paddasslem10  39297  pmodlem1  39314  llnexchb2lem  39336  arglem1N  39658  cdlemd4  39669  cdlemd  39675  cdleme16  39753  cdleme20  39792  cdleme21k  39806  cdleme22cN  39810  cdleme27N  39837  cdleme28c  39840  cdleme29ex  39842  cdleme32fva  39905  cdleme40n  39936  cdlemg15a  40123  cdlemg15  40124  cdlemg16ALTN  40126  cdlemg16z  40127  cdlemg20  40153  cdlemg22  40155  cdlemg29  40173  cdlemg38  40183  cdlemk33N  40377  cdlemk56  40439  fourierdlem77  45562