Theorem simpl13 1246

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  pythagtriplem4  16150  mply1topmatcl  21407  brbtwn2  26685  ax5seg  26718  br8  32987  nolt02o  33194  btwndiff  33483  ifscgr  33500  seglecgr12im  33566  atlatle  36450  cvlcvr1  36469  atbtwn  36576  3dimlem3  36591  3dimlem3OLDN  36592  4atlem3  36726  4atlem11  36739  4atlem12  36742  2lplnj  36750  paddasslem4  36953  paddasslem10  36959  pmodlem1  36976  llnexchb2lem  36998  pclfinclN  37080  arglem1N  37320  cdlemd4  37331  cdlemd  37337  cdleme16  37415  cdleme20  37454  cdleme21k  37468  cdleme22cN  37472  cdleme27N  37499  cdleme28c  37502  cdleme29ex  37504  cdleme32fva  37567  cdleme40n  37598  cdlemg15a  37785  cdlemg15  37786  cdlemg16ALTN  37788  cdlemg16z  37789  cdlemg20  37815  cdlemg22  37817  cdlemg29  37835  cdlemg38  37845  cdlemk56  38101  dihord2pre  38355  ismnu  40590  uzwo4  41308  fourierdlem77  42462