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  16759  pmatcollpw1lem1  22730  pmatcollpw1  22732  mp2pm2mplem2  22763  nolt02o  27675  nogt01o  27676  brbtwn2  28990  ax5seg  29023  3vfriswmgr  30365  br8  35969  ifscgr  36257  seglecgr12im  36323  lkrshp  39475  atlatle  39690  cvlcvr1  39709  atbtwn  39816  3dimlem3  39831  3dimlem3OLDN  39832  1cvratex  39843  llnmlplnN  39909  4atlem3  39966  4atlem3a  39967  4atlem11  39979  4atlem12  39982  cdlemb  40164  paddasslem4  40193  paddasslem10  40199  pmodlem1  40216  llnexchb2lem  40238  arglem1N  40560  cdlemd4  40571  cdlemd  40577  cdleme16  40655  cdleme20  40694  cdleme21k  40708  cdleme22cN  40712  cdleme27N  40739  cdleme28c  40742  cdleme29ex  40744  cdleme32fva  40807  cdleme40n  40838  cdlemg15a  41025  cdlemg15  41026  cdlemg16ALTN  41028  cdlemg16z  41029  cdlemg20  41055  cdlemg22  41057  cdlemg29  41075  cdlemg38  41085  cdlemk33N  41279  cdlemk56  41341  fourierdlem77  46535