Theorem simpl12 1256

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  pythagtriplem4  16788  pmatcollpw1lem1  22764  pmatcollpw1  22766  mp2pm2mplem2  22797  nolt02o  27684  nogt01o  27685  brbtwn2  28999  ax5seg  29032  3vfriswmgr  30373  br8  35991  ifscgr  36279  seglecgr12im  36345  lkrshp  39604  atlatle  39819  cvlcvr1  39838  atbtwn  39945  3dimlem3  39960  3dimlem3OLDN  39961  1cvratex  39972  llnmlplnN  40038  4atlem3  40095  4atlem3a  40096  4atlem11  40108  4atlem12  40111  cdlemb  40293  paddasslem4  40322  paddasslem10  40328  pmodlem1  40345  llnexchb2lem  40367  arglem1N  40689  cdlemd4  40700  cdlemd  40706  cdleme16  40784  cdleme20  40823  cdleme21k  40837  cdleme22cN  40841  cdleme27N  40868  cdleme28c  40871  cdleme29ex  40873  cdleme32fva  40936  cdleme40n  40967  cdlemg15a  41154  cdlemg15  41155  cdlemg16ALTN  41157  cdlemg16z  41158  cdlemg20  41184  cdlemg22  41186  cdlemg29  41204  cdlemg38  41214  cdlemk33N  41408  cdlemk56  41470  fourierdlem77  46633