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 400   ∧ 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 401  df-3an 1105

This theorem is used by:  pythagtriplem4  16883  mply1topmatcl  22971  nolt02o  27868  nogt01o  27869  cofslts  28120  coinitslts  28121  brbtwn2  29264  ax5seg  29297  br8  36256  btwndiff  36527  ifscgr  36544  seglecgr12im  36610  atlatle  40122  cvlcvr1  40141  atbtwn  40248  3dimlem3  40263  3dimlem3OLDN  40264  4atlem3  40398  4atlem11  40411  4atlem12  40414  2lplnj  40422  paddasslem4  40625  paddasslem10  40631  pmodlem1  40648  llnexchb2lem  40670  pclfinclN  40752  arglem1N  40992  cdlemd4  41003  cdlemd  41009  cdleme16  41087  cdleme20  41126  cdleme21k  41140  cdleme22cN  41144  cdleme27N  41171  cdleme28c  41174  cdleme29ex  41176  cdleme32fva  41239  cdleme40n  41270  cdlemg15a  41457  cdlemg15  41458  cdlemg16ALTN  41460  cdlemg16z  41461  cdlemg20  41487  cdlemg22  41489  cdlemg29  41507  cdlemg38  41517  cdlemk56  41773  dihord2pre  42027  ismnu  44999  uzwo4  45801  fourierdlem77  46925