Theorem simpl13 1269

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  pythagtriplem4  16904  mply1topmatcl  22999  nolt02o  27896  nogt01o  27897  cofslts  28148  coinitslts  28149  brbtwn2  29292  ax5seg  29325  br8  36269  btwndiff  36540  ifscgr  36557  seglecgr12im  36623  atlatle  40135  cvlcvr1  40154  atbtwn  40261  3dimlem3  40276  3dimlem3OLDN  40277  4atlem3  40411  4atlem11  40424  4atlem12  40427  2lplnj  40435  paddasslem4  40638  paddasslem10  40644  pmodlem1  40661  llnexchb2lem  40683  pclfinclN  40765  arglem1N  41005  cdlemd4  41016  cdlemd  41022  cdleme16  41100  cdleme20  41139  cdleme21k  41153  cdleme22cN  41157  cdleme27N  41184  cdleme28c  41187  cdleme29ex  41189  cdleme32fva  41252  cdleme40n  41283  cdlemg15a  41470  cdlemg15  41471  cdlemg16ALTN  41473  cdlemg16z  41474  cdlemg20  41500  cdlemg22  41502  cdlemg29  41520  cdlemg38  41530  cdlemk56  41786  dihord2pre  42040  ismnu  45012  uzwo4  45814  fourierdlem77  46938