Theorem simpl13 1247

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

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

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

This theorem is referenced by:  pythagtriplem4  16146  mply1topmatcl  21410  brbtwn2  26699  ax5seg  26732  br8  33105  nolt02o  33312  btwndiff  33601  ifscgr  33618  seglecgr12im  33684  atlatle  36616  cvlcvr1  36635  atbtwn  36742  3dimlem3  36757  3dimlem3OLDN  36758  4atlem3  36892  4atlem11  36905  4atlem12  36908  2lplnj  36916  paddasslem4  37119  paddasslem10  37125  pmodlem1  37142  llnexchb2lem  37164  pclfinclN  37246  arglem1N  37486  cdlemd4  37497  cdlemd  37503  cdleme16  37581  cdleme20  37620  cdleme21k  37634  cdleme22cN  37638  cdleme27N  37665  cdleme28c  37668  cdleme29ex  37670  cdleme32fva  37733  cdleme40n  37764  cdlemg15a  37951  cdlemg15  37952  cdlemg16ALTN  37954  cdlemg16z  37955  cdlemg20  37981  cdlemg22  37983  cdlemg29  38001  cdlemg38  38011  cdlemk56  38267  dihord2pre  38521  ismnu  40969  uzwo4  41687  fourierdlem77  42825