Theorem simpl32 1253

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 1190	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1185	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:  initoeu2lem2  17995  mulmarep1gsum2  22463  tsmsxp  24046  noinfres  27642  ax5seg  28736  br8d  32383  br8  35286  cgrextend  35540  segconeq  35542  trisegint  35560  ifscgr  35576  cgrsub  35577  btwnxfr  35588  seglecgr12im  35642  segletr  35646  exatleN  38814  atbtwn  38856  3dim1  38877  3dim2  38878  2llnjaN  38976  4atlem10b  39015  4atlem11  39019  4atlem12  39022  2lplnj  39030  cdlemb  39204  paddasslem4  39233  pmodlem1  39256  4atex2  39487  trlval3  39597  arglem1N  39600  cdleme0moN  39635  cdleme17b  39697  cdleme20  39734  cdleme21j  39746  cdleme28c  39782  cdleme35h2  39867  cdleme38n  39874  cdlemg6c  40030  cdlemg6  40033  cdlemg7N  40036  cdlemg11a  40047  cdlemg12e  40057  cdlemg16  40067  cdlemg16ALTN  40068  cdlemg16zz  40070  cdlemg20  40095  cdlemg22  40097  cdlemg37  40099  cdlemg31d  40110  cdlemg29  40115  cdlemg33b  40117  cdlemg33  40121  cdlemg39  40126  cdlemg42  40139  cdlemk25-3  40314