Theorem simpl13 1248

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  pythagtriplem4  16448  mply1topmatcl  21862  brbtwn2  27176  ax5seg  27209  br8  33629  poxp3  33723  nolt02o  33825  nogt01o  33826  cofsslt  34015  coinitsslt  34016  btwndiff  34256  ifscgr  34273  seglecgr12im  34339  atlatle  37261  cvlcvr1  37280  atbtwn  37387  3dimlem3  37402  3dimlem3OLDN  37403  4atlem3  37537  4atlem11  37550  4atlem12  37553  2lplnj  37561  paddasslem4  37764  paddasslem10  37770  pmodlem1  37787  llnexchb2lem  37809  pclfinclN  37891  arglem1N  38131  cdlemd4  38142  cdlemd  38148  cdleme16  38226  cdleme20  38265  cdleme21k  38279  cdleme22cN  38283  cdleme27N  38310  cdleme28c  38313  cdleme29ex  38315  cdleme32fva  38378  cdleme40n  38409  cdlemg15a  38596  cdlemg15  38597  cdlemg16ALTN  38599  cdlemg16z  38600  cdlemg20  38626  cdlemg22  38628  cdlemg29  38646  cdlemg38  38656  cdlemk56  38912  dihord2pre  39166  ismnu  41768  uzwo4  42490  fourierdlem77  43614