Theorem simpl13 1252

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  pythagtriplem4  16759  mply1topmatcl  22761  nolt02o  27675  nogt01o  27676  cofslts  27926  coinitslts  27927  brbtwn2  28990  ax5seg  29023  br8  35969  btwndiff  36240  ifscgr  36257  seglecgr12im  36323  atlatle  39693  cvlcvr1  39712  atbtwn  39819  3dimlem3  39834  3dimlem3OLDN  39835  4atlem3  39969  4atlem11  39982  4atlem12  39985  2lplnj  39993  paddasslem4  40196  paddasslem10  40202  pmodlem1  40219  llnexchb2lem  40241  pclfinclN  40323  arglem1N  40563  cdlemd4  40574  cdlemd  40580  cdleme16  40658  cdleme20  40697  cdleme21k  40711  cdleme22cN  40715  cdleme27N  40742  cdleme28c  40745  cdleme29ex  40747  cdleme32fva  40810  cdleme40n  40841  cdlemg15a  41028  cdlemg15  41029  cdlemg16ALTN  41031  cdlemg16z  41032  cdlemg20  41058  cdlemg22  41060  cdlemg29  41078  cdlemg38  41088  cdlemk56  41344  dihord2pre  41598  ismnu  44614  uzwo4  45410  fourierdlem77  46538