Theorem simpl12 1266

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  pythagtriplem4  16869  pmatcollpw1lem1  22892  pmatcollpw1  22894  mp2pm2mplem2  22925  nolt02o  27817  nogt01o  27818  brbtwn2  29164  ax5seg  29197  3vfriswmgr  30538  br8  36119  ifscgr  36407  seglecgr12im  36473  lkrshp  39741  atlatle  39956  cvlcvr1  39975  atbtwn  40082  3dimlem3  40097  3dimlem3OLDN  40098  1cvratex  40109  llnmlplnN  40175  4atlem3  40232  4atlem3a  40233  4atlem11  40245  4atlem12  40248  cdlemb  40430  paddasslem4  40459  paddasslem10  40465  pmodlem1  40482  llnexchb2lem  40504  arglem1N  40826  cdlemd4  40837  cdlemd  40843  cdleme16  40921  cdleme20  40960  cdleme21k  40974  cdleme22cN  40978  cdleme27N  41005  cdleme28c  41008  cdleme29ex  41010  cdleme32fva  41073  cdleme40n  41104  cdlemg15a  41291  cdlemg15  41292  cdlemg16ALTN  41294  cdlemg16z  41295  cdlemg20  41321  cdlemg22  41323  cdlemg29  41341  cdlemg38  41351  cdlemk33N  41545  cdlemk56  41607  fourierdlem77  46755