Theorem simpl13 1248

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  pythagtriplem4  16787  mply1topmatcl  22706  nolt02o  27627  nogt01o  27628  cofsslt  27837  coinitsslt  27838  brbtwn2  28715  ax5seg  28748  br8  35350  btwndiff  35623  ifscgr  35640  seglecgr12im  35706  atlatle  38792  cvlcvr1  38811  atbtwn  38919  3dimlem3  38934  3dimlem3OLDN  38935  4atlem3  39069  4atlem11  39082  4atlem12  39085  2lplnj  39093  paddasslem4  39296  paddasslem10  39302  pmodlem1  39319  llnexchb2lem  39341  pclfinclN  39423  arglem1N  39663  cdlemd4  39674  cdlemd  39680  cdleme16  39758  cdleme20  39797  cdleme21k  39811  cdleme22cN  39815  cdleme27N  39842  cdleme28c  39845  cdleme29ex  39847  cdleme32fva  39910  cdleme40n  39941  cdlemg15a  40128  cdlemg15  40129  cdlemg16ALTN  40131  cdlemg16z  40132  cdlemg20  40158  cdlemg22  40160  cdlemg29  40178  cdlemg38  40188  cdlemk56  40444  dihord2pre  40698  ismnu  43698  uzwo4  44417  fourierdlem77  45571