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  16448  pmatcollpw1lem1  21831  pmatcollpw1  21833  mp2pm2mplem2  21864  brbtwn2  27176  ax5seg  27209  3vfriswmgr  28543  br8  33629  poxp3  33723  nolt02o  33825  nogt01o  33826  ifscgr  34273  seglecgr12im  34339  lkrshp  37046  atlatle  37261  cvlcvr1  37280  atbtwn  37387  3dimlem3  37402  3dimlem3OLDN  37403  1cvratex  37414  llnmlplnN  37480  4atlem3  37537  4atlem3a  37538  4atlem11  37550  4atlem12  37553  cdlemb  37735  paddasslem4  37764  paddasslem10  37770  pmodlem1  37787  llnexchb2lem  37809  arglem1N  38131  cdlemd4  38142  cdlemd  38148  cdleme16  38226  cdleme20  38265  cdleme21k  38279  cdleme22cN  38283  cdleme27N  38310  cdleme28c  38313  cdleme29ex  38315  cdleme32fva  38378  cdleme40n  38409  cdlemg15a  38596  cdlemg15  38597  cdlemg16ALTN  38599  cdlemg16z  38600  cdlemg20  38626  cdlemg22  38628  cdlemg29  38646  cdlemg38  38656  cdlemk33N  38850  cdlemk56  38912  fourierdlem77  43614