Theorem simpl32 1255

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1187	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  18082  mulmarep1gsum2  22601  tsmsxp  24184  noinfres  27785  ax5seg  28971  br8d  32632  br8  35718  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  btwnxfr  36020  seglecgr12im  36074  segletr  36078  exatleN  39361  atbtwn  39403  3dim1  39424  3dim2  39425  2llnjaN  39523  4atlem10b  39562  4atlem11  39566  4atlem12  39569  2lplnj  39577  cdlemb  39751  paddasslem4  39780  pmodlem1  39803  4atex2  40034  trlval3  40144  arglem1N  40147  cdleme0moN  40182  cdleme17b  40244  cdleme20  40281  cdleme21j  40293  cdleme28c  40329  cdleme35h2  40414  cdleme38n  40421  cdlemg6c  40577  cdlemg6  40580  cdlemg7N  40583  cdlemg11a  40594  cdlemg12e  40604  cdlemg16  40614  cdlemg16ALTN  40615  cdlemg16zz  40617  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg31d  40657  cdlemg29  40662  cdlemg33b  40664  cdlemg33  40668  cdlemg39  40673  cdlemg42  40686  cdlemk25-3  40861