Theorem simpl12 1268

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16904  pmatcollpw1lem1  22968  pmatcollpw1  22970  mp2pm2mplem2  23001  nolt02o  27896  nogt01o  27897  brbtwn2  29292  ax5seg  29325  3vfriswmgr  30666  br8  36269  ifscgr  36557  seglecgr12im  36623  lkrshp  39920  atlatle  40135  cvlcvr1  40154  atbtwn  40261  3dimlem3  40276  3dimlem3OLDN  40277  1cvratex  40288  llnmlplnN  40354  4atlem3  40411  4atlem3a  40412  4atlem11  40424  4atlem12  40427  cdlemb  40609  paddasslem4  40638  paddasslem10  40644  pmodlem1  40661  llnexchb2lem  40683  arglem1N  41005  cdlemd4  41016  cdlemd  41022  cdleme16  41100  cdleme20  41139  cdleme21k  41153  cdleme22cN  41157  cdleme27N  41184  cdleme28c  41187  cdleme29ex  41189  cdleme32fva  41252  cdleme40n  41283  cdlemg15a  41470  cdlemg15  41471  cdlemg16ALTN  41473  cdlemg16z  41474  cdlemg20  41500  cdlemg22  41502  cdlemg29  41520  cdlemg38  41530  cdlemk33N  41724  cdlemk56  41786  fourierdlem77  46938