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  16731  mply1topmatcl  22721  nolt02o  27635  nogt01o  27636  cofsslt  27863  coinitsslt  27864  brbtwn2  28884  ax5seg  28917  br8  35798  btwndiff  36067  ifscgr  36084  seglecgr12im  36150  atlatle  39365  cvlcvr1  39384  atbtwn  39491  3dimlem3  39506  3dimlem3OLDN  39507  4atlem3  39641  4atlem11  39654  4atlem12  39657  2lplnj  39665  paddasslem4  39868  paddasslem10  39874  pmodlem1  39891  llnexchb2lem  39913  pclfinclN  39995  arglem1N  40235  cdlemd4  40246  cdlemd  40252  cdleme16  40330  cdleme20  40369  cdleme21k  40383  cdleme22cN  40387  cdleme27N  40414  cdleme28c  40417  cdleme29ex  40419  cdleme32fva  40482  cdleme40n  40513  cdlemg15a  40700  cdlemg15  40701  cdlemg16ALTN  40703  cdlemg16z  40704  cdlemg20  40730  cdlemg22  40732  cdlemg29  40750  cdlemg38  40760  cdlemk56  41016  dihord2pre  41270  ismnu  44300  uzwo4  45096  fourierdlem77  46227