Theorem simpl12 1262

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  pythagtriplem4  16838  pmatcollpw1lem1  22814  pmatcollpw1  22816  mp2pm2mplem2  22847  nolt02o  27736  nogt01o  27737  brbtwn2  29052  ax5seg  29085  3vfriswmgr  30426  br8  36070  ifscgr  36358  seglecgr12im  36424  lkrshp  39693  atlatle  39908  cvlcvr1  39927  atbtwn  40034  3dimlem3  40049  3dimlem3OLDN  40050  1cvratex  40061  llnmlplnN  40127  4atlem3  40184  4atlem3a  40185  4atlem11  40197  4atlem12  40200  cdlemb  40382  paddasslem4  40411  paddasslem10  40417  pmodlem1  40434  llnexchb2lem  40456  arglem1N  40778  cdlemd4  40789  cdlemd  40795  cdleme16  40873  cdleme20  40912  cdleme21k  40926  cdleme22cN  40930  cdleme27N  40957  cdleme28c  40960  cdleme29ex  40962  cdleme32fva  41025  cdleme40n  41056  cdlemg15a  41243  cdlemg15  41244  cdlemg16ALTN  41246  cdlemg16z  41247  cdlemg20  41273  cdlemg22  41275  cdlemg29  41293  cdlemg38  41303  cdlemk33N  41497  cdlemk56  41559  fourierdlem77  46721