Theorem simpl12 1317

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  pythagtriplem4  15746  pmatcollpw1lem1  20801  pmatcollpw1  20803  mp2pm2mplem2  20834  brbtwn2  26005  ax5seg  26038  3vfriswmgr  27453  br8  31974  nolt02o  32172  ifscgr  32478  seglecgr12im  32544  lkrshp  34913  atlatle  35128  cvlcvr1  35147  atbtwn  35253  3dimlem3  35268  3dimlem3OLDN  35269  1cvratex  35280  llnmlplnN  35346  4atlem3  35403  4atlem3a  35404  4atlem11  35416  4atlem12  35419  cdlemb  35601  paddasslem4  35630  paddasslem10  35636  pmodlem1  35653  llnexchb2lem  35675  arglem1N  35998  cdlemd4  36009  cdlemd  36015  cdleme16  36093  cdleme20  36132  cdleme21k  36146  cdleme22cN  36150  cdleme27N  36177  cdleme28c  36180  cdleme29ex  36182  cdleme32fva  36245  cdleme40n  36276  cdlemg15a  36463  cdlemg15  36464  cdlemg16ALTN  36466  cdlemg16z  36467  cdlemg20  36493  cdlemg22  36495  cdlemg29  36513  cdlemg38  36523  cdlemk33N  36717  cdlemk56  36779  fourierdlem77  40921