Theorem simpl13 1250

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 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜒)
2	1	3ad2antl1 1185	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  16866  mply1topmatcl  22832  nolt02o  27758  nogt01o  27759  cofsslt  27970  coinitsslt  27971  brbtwn2  28938  ax5seg  28971  br8  35718  btwndiff  35991  ifscgr  36008  seglecgr12im  36074  atlatle  39276  cvlcvr1  39295  atbtwn  39403  3dimlem3  39418  3dimlem3OLDN  39419  4atlem3  39553  4atlem11  39566  4atlem12  39569  2lplnj  39577  paddasslem4  39780  paddasslem10  39786  pmodlem1  39803  llnexchb2lem  39825  pclfinclN  39907  arglem1N  40147  cdlemd4  40158  cdlemd  40164  cdleme16  40242  cdleme20  40281  cdleme21k  40295  cdleme22cN  40299  cdleme27N  40326  cdleme28c  40329  cdleme29ex  40331  cdleme32fva  40394  cdleme40n  40425  cdlemg15a  40612  cdlemg15  40613  cdlemg16ALTN  40615  cdlemg16z  40616  cdlemg20  40642  cdlemg22  40644  cdlemg29  40662  cdlemg38  40672  cdlemk56  40928  dihord2pre  41182  ismnu  44230  uzwo4  44955  fourierdlem77  46104