Theorem simpl13 1337

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

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1111

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 199  df-an 387  df-3an 1113

This theorem is referenced by:  pythagtriplem4  15895  mply1topmatcl  20980  brbtwn2  26204  ax5seg  26237  br8  32177  nolt02o  32373  btwndiff  32662  ifscgr  32679  seglecgr12im  32745  atlatle  35388  cvlcvr1  35407  atbtwn  35514  3dimlem3  35529  3dimlem3OLDN  35530  4atlem3  35664  4atlem11  35677  4atlem12  35680  2lplnj  35688  paddasslem4  35891  paddasslem10  35897  pmodlem1  35914  llnexchb2lem  35936  pclfinclN  36018  arglem1N  36258  cdlemd4  36269  cdlemd  36275  cdleme16  36353  cdleme20  36392  cdleme21k  36406  cdleme22cN  36410  cdleme27N  36437  cdleme28c  36440  cdleme29ex  36442  cdleme32fva  36505  cdleme40n  36536  cdlemg15a  36723  cdlemg15  36724  cdlemg16ALTN  36726  cdlemg16z  36727  cdlemg20  36753  cdlemg22  36755  cdlemg29  36773  cdlemg38  36783  cdlemk56  37039  dihord2pre  37293  uzwo4  40031  fourierdlem77  41187