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  16790  pmatcollpw1lem1  22739  pmatcollpw1  22741  mp2pm2mplem2  22772  nolt02o  27659  nogt01o  27660  brbtwn2  28974  ax5seg  29007  3vfriswmgr  30348  br8  35938  ifscgr  36226  seglecgr12im  36292  lkrshp  39551  atlatle  39766  cvlcvr1  39785  atbtwn  39892  3dimlem3  39907  3dimlem3OLDN  39908  1cvratex  39919  llnmlplnN  39985  4atlem3  40042  4atlem3a  40043  4atlem11  40055  4atlem12  40058  cdlemb  40240  paddasslem4  40269  paddasslem10  40275  pmodlem1  40292  llnexchb2lem  40314  arglem1N  40636  cdlemd4  40647  cdlemd  40653  cdleme16  40731  cdleme20  40770  cdleme21k  40784  cdleme22cN  40788  cdleme27N  40815  cdleme28c  40818  cdleme29ex  40820  cdleme32fva  40883  cdleme40n  40914  cdlemg15a  41101  cdlemg15  41102  cdlemg16ALTN  41104  cdlemg16z  41105  cdlemg20  41131  cdlemg22  41133  cdlemg29  41151  cdlemg38  41161  cdlemk33N  41355  cdlemk56  41417  fourierdlem77  46611