Theorem simpl12 1248

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16520  pmatcollpw1lem1  21923  pmatcollpw1  21925  mp2pm2mplem2  21956  brbtwn2  27273  ax5seg  27306  3vfriswmgr  28642  br8  33723  poxp3  33796  nolt02o  33898  nogt01o  33899  ifscgr  34346  seglecgr12im  34412  lkrshp  37119  atlatle  37334  cvlcvr1  37353  atbtwn  37460  3dimlem3  37475  3dimlem3OLDN  37476  1cvratex  37487  llnmlplnN  37553  4atlem3  37610  4atlem3a  37611  4atlem11  37623  4atlem12  37626  cdlemb  37808  paddasslem4  37837  paddasslem10  37843  pmodlem1  37860  llnexchb2lem  37882  arglem1N  38204  cdlemd4  38215  cdlemd  38221  cdleme16  38299  cdleme20  38338  cdleme21k  38352  cdleme22cN  38356  cdleme27N  38383  cdleme28c  38386  cdleme29ex  38388  cdleme32fva  38451  cdleme40n  38482  cdlemg15a  38669  cdlemg15  38670  cdlemg16ALTN  38672  cdlemg16z  38673  cdlemg20  38699  cdlemg22  38701  cdlemg29  38719  cdlemg38  38729  cdlemk33N  38923  cdlemk56  38985  fourierdlem77  43724