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  16977  mply1topmatcl  23103  nolt02o  28034  nogt01o  28035  cofslts  28286  coinitslts  28287  brbtwn2  29465  ax5seg  29498  br8  36490  btwndiff  36762  ifscgr  36779  seglecgr12im  36845  atlatle  40345  cvlcvr1  40364  atbtwn  40471  3dimlem3  40486  3dimlem3OLDN  40487  4atlem3  40621  4atlem11  40634  4atlem12  40637  2lplnj  40645  paddasslem4  40848  paddasslem10  40854  pmodlem1  40871  llnexchb2lem  40893  pclfinclN  40975  arglem1N  41215  cdlemd4  41226  cdlemd  41232  cdleme16  41310  cdleme20  41349  cdleme21k  41363  cdleme22cN  41367  cdleme27N  41394  cdleme28c  41397  cdleme29ex  41399  cdleme32fva  41462  cdleme40n  41493  cdlemg15a  41680  cdlemg15  41681  cdlemg16ALTN  41683  cdlemg16z  41684  cdlemg20  41710  cdlemg22  41712  cdlemg29  41730  cdlemg38  41740  cdlemk56  41996  dihord2pre  42250  ismnu  45204  uzwo4  46013  fourierdlem77  47137