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  17029  mply1topmatcl  23156  nolt02o  28085  nogt01o  28086  cofslts  28337  coinitslts  28338  brbtwn2  29516  ax5seg  29549  br8  36712  btwndiff  36983  ifscgr  37000  seglecgr12im  37066  atlatle  40580  cvlcvr1  40599  atbtwn  40706  3dimlem3  40721  3dimlem3OLDN  40722  4atlem3  40856  4atlem11  40869  4atlem12  40872  2lplnj  40880  paddasslem4  41083  paddasslem10  41089  pmodlem1  41106  llnexchb2lem  41128  pclfinclN  41210  arglem1N  41450  cdlemd4  41461  cdlemd  41467  cdleme16  41545  cdleme20  41584  cdleme21k  41598  cdleme22cN  41602  cdleme27N  41629  cdleme28c  41632  cdleme29ex  41634  cdleme32fva  41697  cdleme40n  41728  cdlemg15a  41915  cdlemg15  41916  cdlemg16ALTN  41918  cdlemg16z  41919  cdlemg20  41945  cdlemg22  41947  cdlemg29  41965  cdlemg38  41975  cdlemk56  42231  dihord2pre  42485  ismnu  45448  uzwo4  46286  fourierdlem77  47408