Theorem simpl13 1319

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 197  df-an 385  df-3an 1074

This theorem is referenced by:  pythagtriplem4  15726  mply1topmatcl  20812  brbtwn2  25984  ax5seg  26017  br8  31953  nolt02o  32151  btwndiff  32440  ifscgr  32457  seglecgr12im  32523  atlatle  35110  cvlcvr1  35129  atbtwn  35235  3dimlem3  35250  3dimlem3OLDN  35251  4atlem3  35385  4atlem11  35398  4atlem12  35401  2lplnj  35409  paddasslem4  35612  paddasslem10  35618  pmodlem1  35635  llnexchb2lem  35657  pclfinclN  35739  arglem1N  35980  cdlemd4  35991  cdlemd  35997  cdleme16  36075  cdleme20  36114  cdleme21k  36128  cdleme22cN  36132  cdleme27N  36159  cdleme28c  36162  cdleme29ex  36164  cdleme32fva  36227  cdleme40n  36258  cdlemg15a  36445  cdlemg15  36446  cdlemg16ALTN  36448  cdlemg16z  36449  cdlemg20  36475  cdlemg22  36477  cdlemg29  36495  cdlemg38  36505  cdlemk56  36761  dihord2pre  37016  uzwo4  39720  fourierdlem77  40903