Theorem simpl12 1245

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pythagtriplem4  16158  pmatcollpw1lem1  21384  pmatcollpw1  21386  mp2pm2mplem2  21417  brbtwn2  26693  ax5seg  26726  3vfriswmgr  28059  br8  32994  nolt02o  33201  ifscgr  33507  seglecgr12im  33573  lkrshp  36243  atlatle  36458  cvlcvr1  36477  atbtwn  36584  3dimlem3  36599  3dimlem3OLDN  36600  1cvratex  36611  llnmlplnN  36677  4atlem3  36734  4atlem3a  36735  4atlem11  36747  4atlem12  36750  cdlemb  36932  paddasslem4  36961  paddasslem10  36967  pmodlem1  36984  llnexchb2lem  37006  arglem1N  37328  cdlemd4  37339  cdlemd  37345  cdleme16  37423  cdleme20  37462  cdleme21k  37476  cdleme22cN  37480  cdleme27N  37507  cdleme28c  37510  cdleme29ex  37512  cdleme32fva  37575  cdleme40n  37606  cdlemg15a  37793  cdlemg15  37794  cdlemg16ALTN  37796  cdlemg16z  37797  cdlemg20  37823  cdlemg22  37825  cdlemg29  37843  cdlemg38  37853  cdlemk33N  38047  cdlemk56  38109  fourierdlem77  42475