Theorem simpl12 1251

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  pythagtriplem4  16781  pmatcollpw1lem1  22749  pmatcollpw1  22751  mp2pm2mplem2  22782  nolt02o  27673  nogt01o  27674  brbtwn2  28988  ax5seg  29021  3vfriswmgr  30363  br8  35954  ifscgr  36242  seglecgr12im  36308  lkrshp  39565  atlatle  39780  cvlcvr1  39799  atbtwn  39906  3dimlem3  39921  3dimlem3OLDN  39922  1cvratex  39933  llnmlplnN  39999  4atlem3  40056  4atlem3a  40057  4atlem11  40069  4atlem12  40072  cdlemb  40254  paddasslem4  40283  paddasslem10  40289  pmodlem1  40306  llnexchb2lem  40328  arglem1N  40650  cdlemd4  40661  cdlemd  40667  cdleme16  40745  cdleme20  40784  cdleme21k  40798  cdleme22cN  40802  cdleme27N  40829  cdleme28c  40832  cdleme29ex  40834  cdleme32fva  40897  cdleme40n  40928  cdlemg15a  41115  cdlemg15  41116  cdlemg16ALTN  41118  cdlemg16z  41119  cdlemg20  41145  cdlemg22  41147  cdlemg29  41165  cdlemg38  41175  cdlemk33N  41369  cdlemk56  41431  fourierdlem77  46629