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  16917  pmatcollpw1lem1  23005  pmatcollpw1  23007  mp2pm2mplem2  23038  nolt02o  27939  nogt01o  27940  brbtwn2  29370  ax5seg  29403  3vfriswmgr  30766  br8  36343  ifscgr  36632  seglecgr12im  36698  lkrshp  39986  atlatle  40201  cvlcvr1  40220  atbtwn  40327  3dimlem3  40342  3dimlem3OLDN  40343  1cvratex  40354  llnmlplnN  40420  4atlem3  40477  4atlem3a  40478  4atlem11  40490  4atlem12  40493  cdlemb  40675  paddasslem4  40704  paddasslem10  40710  pmodlem1  40727  llnexchb2lem  40749  arglem1N  41071  cdlemd4  41082  cdlemd  41088  cdleme16  41166  cdleme20  41205  cdleme21k  41219  cdleme22cN  41223  cdleme27N  41250  cdleme28c  41253  cdleme29ex  41255  cdleme32fva  41318  cdleme40n  41349  cdlemg15a  41536  cdlemg15  41537  cdlemg16ALTN  41539  cdlemg16z  41540  cdlemg20  41566  cdlemg22  41568  cdlemg29  41586  cdlemg38  41596  cdlemk33N  41790  cdlemk56  41852  fourierdlem77  47019