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 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜓)

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

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 1105

This theorem is referenced by:  pythagtriplem4  16880  pmatcollpw1lem1  22912  pmatcollpw1  22914  mp2pm2mplem2  22945  nolt02o  27837  nogt01o  27838  brbtwn2  29233  ax5seg  29266  3vfriswmgr  30607  br8  36226  ifscgr  36514  seglecgr12im  36580  lkrshp  39857  atlatle  40072  cvlcvr1  40091  atbtwn  40198  3dimlem3  40213  3dimlem3OLDN  40214  1cvratex  40225  llnmlplnN  40291  4atlem3  40348  4atlem3a  40349  4atlem11  40361  4atlem12  40364  cdlemb  40546  paddasslem4  40575  paddasslem10  40581  pmodlem1  40598  llnexchb2lem  40620  arglem1N  40942  cdlemd4  40953  cdlemd  40959  cdleme16  41037  cdleme20  41076  cdleme21k  41090  cdleme22cN  41094  cdleme27N  41121  cdleme28c  41124  cdleme29ex  41126  cdleme32fva  41189  cdleme40n  41220  cdlemg15a  41407  cdlemg15  41408  cdlemg16ALTN  41410  cdlemg16z  41411  cdlemg20  41437  cdlemg22  41439  cdlemg29  41457  cdlemg38  41467  cdlemk33N  41661  cdlemk56  41723  fourierdlem77  46877