Theorem simpl13 1249

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl13	⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

Proof of Theorem simpl13

Step	Hyp	Ref	Expression
1		simpl3 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl1 1184	1 ⊢ ((((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜃 ∧ 𝜏) ∧ 𝜂) → 𝜒)

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

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16530  mply1topmatcl  21964  brbtwn2  27283  ax5seg  27316  br8  33731  poxp3  33804  nolt02o  33906  nogt01o  33907  cofsslt  34096  coinitsslt  34097  btwndiff  34337  ifscgr  34354  seglecgr12im  34420  atlatle  37342  cvlcvr1  37361  atbtwn  37468  3dimlem3  37483  3dimlem3OLDN  37484  4atlem3  37618  4atlem11  37631  4atlem12  37634  2lplnj  37642  paddasslem4  37845  paddasslem10  37851  pmodlem1  37868  llnexchb2lem  37890  pclfinclN  37972  arglem1N  38212  cdlemd4  38223  cdlemd  38229  cdleme16  38307  cdleme20  38346  cdleme21k  38360  cdleme22cN  38364  cdleme27N  38391  cdleme28c  38394  cdleme29ex  38396  cdleme32fva  38459  cdleme40n  38490  cdlemg15a  38677  cdlemg15  38678  cdlemg16ALTN  38680  cdlemg16z  38681  cdlemg20  38707  cdlemg22  38709  cdlemg29  38727  cdlemg38  38737  cdlemk56  38993  dihord2pre  39247  ismnu  41860  uzwo4  42582  fourierdlem77  43705