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  17029  pmatcollpw1lem1  23125  pmatcollpw1  23127  mp2pm2mplem2  23158  nolt02o  28085  nogt01o  28086  brbtwn2  29516  ax5seg  29549  3vfriswmgr  30912  br8  36712  ifscgr  37000  seglecgr12im  37066  lkrshp  40365  atlatle  40580  cvlcvr1  40599  atbtwn  40706  3dimlem3  40721  3dimlem3OLDN  40722  1cvratex  40733  llnmlplnN  40799  4atlem3  40856  4atlem3a  40857  4atlem11  40869  4atlem12  40872  cdlemb  41054  paddasslem4  41083  paddasslem10  41089  pmodlem1  41106  llnexchb2lem  41128  arglem1N  41450  cdlemd4  41461  cdlemd  41467  cdleme16  41545  cdleme20  41584  cdleme21k  41598  cdleme22cN  41602  cdleme27N  41629  cdleme28c  41632  cdleme29ex  41634  cdleme32fva  41697  cdleme40n  41728  cdlemg15a  41915  cdlemg15  41916  cdlemg16ALTN  41918  cdlemg16z  41919  cdlemg20  41945  cdlemg22  41947  cdlemg29  41965  cdlemg38  41975  cdlemk33N  42169  cdlemk56  42231  fourierdlem77  47408