Theorem simpl12 1245

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pythagtriplem4  16156  pmatcollpw1lem1  21382  pmatcollpw1  21384  mp2pm2mplem2  21415  brbtwn2  26691  ax5seg  26724  3vfriswmgr  28057  br8  32992  nolt02o  33199  ifscgr  33505  seglecgr12im  33571  lkrshp  36256  atlatle  36471  cvlcvr1  36490  atbtwn  36597  3dimlem3  36612  3dimlem3OLDN  36613  1cvratex  36624  llnmlplnN  36690  4atlem3  36747  4atlem3a  36748  4atlem11  36760  4atlem12  36763  cdlemb  36945  paddasslem4  36974  paddasslem10  36980  pmodlem1  36997  llnexchb2lem  37019  arglem1N  37341  cdlemd4  37352  cdlemd  37358  cdleme16  37436  cdleme20  37475  cdleme21k  37489  cdleme22cN  37493  cdleme27N  37520  cdleme28c  37523  cdleme29ex  37525  cdleme32fva  37588  cdleme40n  37619  cdlemg15a  37806  cdlemg15  37807  cdlemg16ALTN  37809  cdlemg16z  37810  cdlemg20  37836  cdlemg22  37838  cdlemg29  37856  cdlemg38  37866  cdlemk33N  38060  cdlemk56  38122  fourierdlem77  42488