Theorem simpl32 1272

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl32	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Proof of Theorem simpl32

Step	Hyp	Ref	Expression
1		simpl2 1209	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1204	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  initoeu2lem2  18060  mulmarep1gsum2  22688  tsmsxp  24269  noinfres  27840  ax5seg  29193  br8d  32861  br8  36114  cgrextend  36366  segconeq  36368  trisegint  36386  ifscgr  36402  cgrsub  36403  btwnxfr  36414  seglecgr12im  36468  segletr  36472  exatleN  40035  atbtwn  40077  3dim1  40098  3dim2  40099  2llnjaN  40197  4atlem10b  40236  4atlem11  40240  4atlem12  40243  2lplnj  40251  cdlemb  40425  paddasslem4  40454  pmodlem1  40477  4atex2  40708  trlval3  40818  arglem1N  40821  cdleme0moN  40856  cdleme17b  40918  cdleme20  40955  cdleme21j  40967  cdleme28c  41003  cdleme35h2  41088  cdleme38n  41095  cdlemg6c  41251  cdlemg6  41254  cdlemg7N  41257  cdlemg11a  41268  cdlemg12e  41278  cdlemg16  41288  cdlemg16ALTN  41289  cdlemg16zz  41291  cdlemg20  41316  cdlemg22  41318  cdlemg37  41320  cdlemg31d  41331  cdlemg29  41336  cdlemg33b  41338  cdlemg33  41342  cdlemg39  41347  cdlemg42  41360  cdlemk25-3  41535