Theorem simpl13 1269

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16917  mply1topmatcl  23036  nolt02o  27939  nogt01o  27940  cofslts  28191  coinitslts  28192  brbtwn2  29370  ax5seg  29403  br8  36343  btwndiff  36615  ifscgr  36632  seglecgr12im  36698  atlatle  40201  cvlcvr1  40220  atbtwn  40327  3dimlem3  40342  3dimlem3OLDN  40343  4atlem3  40477  4atlem11  40490  4atlem12  40493  2lplnj  40501  paddasslem4  40704  paddasslem10  40710  pmodlem1  40727  llnexchb2lem  40749  pclfinclN  40831  arglem1N  41071  cdlemd4  41082  cdlemd  41088  cdleme16  41166  cdleme20  41205  cdleme21k  41219  cdleme22cN  41223  cdleme27N  41250  cdleme28c  41253  cdleme29ex  41255  cdleme32fva  41318  cdleme40n  41349  cdlemg15a  41536  cdlemg15  41537  cdlemg16ALTN  41539  cdlemg16z  41540  cdlemg20  41566  cdlemg22  41568  cdlemg29  41586  cdlemg38  41596  cdlemk56  41852  dihord2pre  42106  ismnu  45093  uzwo4  45895  fourierdlem77  47019