Theorem simpl13 1263

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 400  df-3an 1099

This theorem is referenced by:  pythagtriplem4  16845  mply1topmatcl  22852  nolt02o  27746  nogt01o  27747  cofslts  27998  coinitslts  27999  brbtwn2  29062  ax5seg  29095  br8  36066  btwndiff  36337  ifscgr  36354  seglecgr12im  36420  atlatle  39904  cvlcvr1  39923  atbtwn  40030  3dimlem3  40045  3dimlem3OLDN  40046  4atlem3  40180  4atlem11  40193  4atlem12  40196  2lplnj  40204  paddasslem4  40407  paddasslem10  40413  pmodlem1  40430  llnexchb2lem  40452  pclfinclN  40534  arglem1N  40774  cdlemd4  40785  cdlemd  40791  cdleme16  40869  cdleme20  40908  cdleme21k  40922  cdleme22cN  40926  cdleme27N  40953  cdleme28c  40956  cdleme29ex  40958  cdleme32fva  41021  cdleme40n  41052  cdlemg15a  41239  cdlemg15  41240  cdlemg16ALTN  41242  cdlemg16z  41243  cdlemg20  41269  cdlemg22  41271  cdlemg29  41289  cdlemg38  41299  cdlemk56  41555  dihord2pre  41809  ismnu  44797  uzwo4  45593  fourierdlem77  46717