Theorem simpl13 1257

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  pythagtriplem4  16788  mply1topmatcl  22795  nolt02o  27684  nogt01o  27685  cofslts  27935  coinitslts  27936  brbtwn2  28999  ax5seg  29032  br8  35991  btwndiff  36262  ifscgr  36279  seglecgr12im  36345  atlatle  39819  cvlcvr1  39838  atbtwn  39945  3dimlem3  39960  3dimlem3OLDN  39961  4atlem3  40095  4atlem11  40108  4atlem12  40111  2lplnj  40119  paddasslem4  40322  paddasslem10  40328  pmodlem1  40345  llnexchb2lem  40367  pclfinclN  40449  arglem1N  40689  cdlemd4  40700  cdlemd  40706  cdleme16  40784  cdleme20  40823  cdleme21k  40837  cdleme22cN  40841  cdleme27N  40868  cdleme28c  40871  cdleme29ex  40873  cdleme32fva  40936  cdleme40n  40967  cdlemg15a  41154  cdlemg15  41155  cdlemg16ALTN  41157  cdlemg16z  41158  cdlemg20  41184  cdlemg22  41186  cdlemg29  41204  cdlemg38  41214  cdlemk56  41470  dihord2pre  41724  ismnu  44712  uzwo4  45508  fourierdlem77  46633