Theorem simpl13 1267

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 401  df-3an 1103

This theorem is referenced by:  pythagtriplem4  16867  mply1topmatcl  22919  nolt02o  27813  nogt01o  27814  cofslts  28065  coinitslts  28066  brbtwn2  29160  ax5seg  29193  br8  36114  btwndiff  36385  ifscgr  36402  seglecgr12im  36468  atlatle  39951  cvlcvr1  39970  atbtwn  40077  3dimlem3  40092  3dimlem3OLDN  40093  4atlem3  40227  4atlem11  40240  4atlem12  40243  2lplnj  40251  paddasslem4  40454  paddasslem10  40460  pmodlem1  40477  llnexchb2lem  40499  pclfinclN  40581  arglem1N  40821  cdlemd4  40832  cdlemd  40838  cdleme16  40916  cdleme20  40955  cdleme21k  40969  cdleme22cN  40973  cdleme27N  41000  cdleme28c  41003  cdleme29ex  41005  cdleme32fva  41068  cdleme40n  41099  cdlemg15a  41286  cdlemg15  41287  cdlemg16ALTN  41289  cdlemg16z  41290  cdlemg20  41316  cdlemg22  41318  cdlemg29  41336  cdlemg38  41346  cdlemk56  41602  dihord2pre  41856  ismnu  44830  uzwo4  45632  fourierdlem77  46756