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  16741  mply1topmatcl  22730  nolt02o  27644  nogt01o  27645  cofsslt  27872  coinitsslt  27873  brbtwn2  28894  ax5seg  28927  br8  35811  btwndiff  36082  ifscgr  36099  seglecgr12im  36165  atlatle  39429  cvlcvr1  39448  atbtwn  39555  3dimlem3  39570  3dimlem3OLDN  39571  4atlem3  39705  4atlem11  39718  4atlem12  39721  2lplnj  39729  paddasslem4  39932  paddasslem10  39938  pmodlem1  39955  llnexchb2lem  39977  pclfinclN  40059  arglem1N  40299  cdlemd4  40310  cdlemd  40316  cdleme16  40394  cdleme20  40433  cdleme21k  40447  cdleme22cN  40451  cdleme27N  40478  cdleme28c  40481  cdleme29ex  40483  cdleme32fva  40546  cdleme40n  40577  cdlemg15a  40764  cdlemg15  40765  cdlemg16ALTN  40767  cdlemg16z  40768  cdlemg20  40794  cdlemg22  40796  cdlemg29  40814  cdlemg38  40824  cdlemk56  41080  dihord2pre  41334  ismnu  44368  uzwo4  45164  fourierdlem77  46295