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  16790  pmatcollpw1lem1  22661  pmatcollpw1  22663  mp2pm2mplem2  22694  nolt02o  27607  nogt01o  27608  brbtwn2  28832  ax5seg  28865  3vfriswmgr  30207  br8  35743  ifscgr  36032  seglecgr12im  36098  lkrshp  39098  atlatle  39313  cvlcvr1  39332  atbtwn  39440  3dimlem3  39455  3dimlem3OLDN  39456  1cvratex  39467  llnmlplnN  39533  4atlem3  39590  4atlem3a  39591  4atlem11  39603  4atlem12  39606  cdlemb  39788  paddasslem4  39817  paddasslem10  39823  pmodlem1  39840  llnexchb2lem  39862  arglem1N  40184  cdlemd4  40195  cdlemd  40201  cdleme16  40279  cdleme20  40318  cdleme21k  40332  cdleme22cN  40336  cdleme27N  40363  cdleme28c  40366  cdleme29ex  40368  cdleme32fva  40431  cdleme40n  40462  cdlemg15a  40649  cdlemg15  40650  cdlemg16ALTN  40652  cdlemg16z  40653  cdlemg20  40679  cdlemg22  40681  cdlemg29  40699  cdlemg38  40709  cdlemk33N  40903  cdlemk56  40965  fourierdlem77  46181