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 395   ∧ 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 206  df-an 396  df-3an 1086

This theorem is referenced by:  pythagtriplem4  16748  mply1topmatcl  22617  nolt02o  27532  nogt01o  27533  cofsslt  27742  coinitsslt  27743  brbtwn2  28587  ax5seg  28620  br8  35187  btwndiff  35460  ifscgr  35477  seglecgr12im  35543  atlatle  38646  cvlcvr1  38665  atbtwn  38773  3dimlem3  38788  3dimlem3OLDN  38789  4atlem3  38923  4atlem11  38936  4atlem12  38939  2lplnj  38947  paddasslem4  39150  paddasslem10  39156  pmodlem1  39173  llnexchb2lem  39195  pclfinclN  39277  arglem1N  39517  cdlemd4  39528  cdlemd  39534  cdleme16  39612  cdleme20  39651  cdleme21k  39665  cdleme22cN  39669  cdleme27N  39696  cdleme28c  39699  cdleme29ex  39701  cdleme32fva  39764  cdleme40n  39795  cdlemg15a  39982  cdlemg15  39983  cdlemg16ALTN  39985  cdlemg16z  39986  cdlemg20  40012  cdlemg22  40014  cdlemg29  40032  cdlemg38  40042  cdlemk56  40298  dihord2pre  40552  ismnu  43475  uzwo4  44194  fourierdlem77  45350