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  16781  mply1topmatcl  22780  nolt02o  27673  nogt01o  27674  cofslts  27924  coinitslts  27925  brbtwn2  28988  ax5seg  29021  br8  35954  btwndiff  36225  ifscgr  36242  seglecgr12im  36308  atlatle  39780  cvlcvr1  39799  atbtwn  39906  3dimlem3  39921  3dimlem3OLDN  39922  4atlem3  40056  4atlem11  40069  4atlem12  40072  2lplnj  40080  paddasslem4  40283  paddasslem10  40289  pmodlem1  40306  llnexchb2lem  40328  pclfinclN  40410  arglem1N  40650  cdlemd4  40661  cdlemd  40667  cdleme16  40745  cdleme20  40784  cdleme21k  40798  cdleme22cN  40802  cdleme27N  40829  cdleme28c  40832  cdleme29ex  40834  cdleme32fva  40897  cdleme40n  40928  cdlemg15a  41115  cdlemg15  41116  cdlemg16ALTN  41118  cdlemg16z  41119  cdlemg20  41145  cdlemg22  41147  cdlemg29  41165  cdlemg38  41175  cdlemk56  41431  dihord2pre  41685  ismnu  44706  uzwo4  45502  fourierdlem77  46629