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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  pythagtriplem4  16756  pmatcollpw1lem1  22496  pmatcollpw1  22498  mp2pm2mplem2  22529  nolt02o  27434  nogt01o  27435  brbtwn2  28430  ax5seg  28463  3vfriswmgr  29798  br8  35030  ifscgr  35320  seglecgr12im  35386  lkrshp  38278  atlatle  38493  cvlcvr1  38512  atbtwn  38620  3dimlem3  38635  3dimlem3OLDN  38636  1cvratex  38647  llnmlplnN  38713  4atlem3  38770  4atlem3a  38771  4atlem11  38783  4atlem12  38786  cdlemb  38968  paddasslem4  38997  paddasslem10  39003  pmodlem1  39020  llnexchb2lem  39042  arglem1N  39364  cdlemd4  39375  cdlemd  39381  cdleme16  39459  cdleme20  39498  cdleme21k  39512  cdleme22cN  39516  cdleme27N  39543  cdleme28c  39546  cdleme29ex  39548  cdleme32fva  39611  cdleme40n  39642  cdlemg15a  39829  cdlemg15  39830  cdlemg16ALTN  39832  cdlemg16z  39833  cdlemg20  39859  cdlemg22  39861  cdlemg29  39879  cdlemg38  39889  cdlemk33N  40083  cdlemk56  40145  fourierdlem77  45197