Theorem simpl13 1251

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16790  mply1topmatcl  22692  nolt02o  27607  nogt01o  27608  cofsslt  27826  coinitsslt  27827  brbtwn2  28832  ax5seg  28865  br8  35743  btwndiff  36015  ifscgr  36032  seglecgr12im  36098  atlatle  39313  cvlcvr1  39332  atbtwn  39440  3dimlem3  39455  3dimlem3OLDN  39456  4atlem3  39590  4atlem11  39603  4atlem12  39606  2lplnj  39614  paddasslem4  39817  paddasslem10  39823  pmodlem1  39840  llnexchb2lem  39862  pclfinclN  39944  arglem1N  40184  cdlemd4  40195  cdlemd  40201  cdleme16  40279  cdleme20  40318  cdleme21k  40332  cdleme22cN  40336  cdleme27N  40363  cdleme28c  40366  cdleme29ex  40368  cdleme32fva  40431  cdleme40n  40462  cdlemg15a  40649  cdlemg15  40650  cdlemg16ALTN  40652  cdlemg16z  40653  cdlemg20  40679  cdlemg22  40681  cdlemg29  40699  cdlemg38  40709  cdlemk56  40965  dihord2pre  41219  ismnu  44250  uzwo4  45047  fourierdlem77  46181