Theorem simpl13 1249

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  pythagtriplem4  16529  mply1topmatcl  21963  brbtwn2  27282  ax5seg  27315  br8  33732  poxp3  33805  nolt02o  33907  nogt01o  33908  cofsslt  34097  coinitsslt  34098  btwndiff  34338  ifscgr  34355  seglecgr12im  34421  atlatle  37341  cvlcvr1  37360  atbtwn  37467  3dimlem3  37482  3dimlem3OLDN  37483  4atlem3  37617  4atlem11  37630  4atlem12  37633  2lplnj  37641  paddasslem4  37844  paddasslem10  37850  pmodlem1  37867  llnexchb2lem  37889  pclfinclN  37971  arglem1N  38211  cdlemd4  38222  cdlemd  38228  cdleme16  38306  cdleme20  38345  cdleme21k  38359  cdleme22cN  38363  cdleme27N  38390  cdleme28c  38393  cdleme29ex  38395  cdleme32fva  38458  cdleme40n  38489  cdlemg15a  38676  cdlemg15  38677  cdlemg16ALTN  38679  cdlemg16z  38680  cdlemg20  38706  cdlemg22  38708  cdlemg29  38726  cdlemg38  38736  cdlemk56  38992  dihord2pre  39246  ismnu  41886  uzwo4  42608  fourierdlem77  43731