Theorem simpl32 1256

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 1193	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1188	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜓)

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

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  initoeu2lem2  18060  mulmarep1gsum2  22580  tsmsxp  24163  noinfres  27767  ax5seg  28953  br8d  32622  br8  35756  cgrextend  36009  segconeq  36011  trisegint  36029  ifscgr  36045  cgrsub  36046  btwnxfr  36057  seglecgr12im  36111  segletr  36115  exatleN  39406  atbtwn  39448  3dim1  39469  3dim2  39470  2llnjaN  39568  4atlem10b  39607  4atlem11  39611  4atlem12  39614  2lplnj  39622  cdlemb  39796  paddasslem4  39825  pmodlem1  39848  4atex2  40079  trlval3  40189  arglem1N  40192  cdleme0moN  40227  cdleme17b  40289  cdleme20  40326  cdleme21j  40338  cdleme28c  40374  cdleme35h2  40459  cdleme38n  40466  cdlemg6c  40622  cdlemg6  40625  cdlemg7N  40628  cdlemg11a  40639  cdlemg12e  40649  cdlemg16  40659  cdlemg16ALTN  40660  cdlemg16zz  40662  cdlemg20  40687  cdlemg22  40689  cdlemg37  40691  cdlemg31d  40702  cdlemg29  40707  cdlemg33b  40709  cdlemg33  40713  cdlemg39  40718  cdlemg42  40731  cdlemk25-3  40906