Theorem simpl32 1257

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 1194	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜓)
2	1	3ad2antl3 1189	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  17973  mulmarep1gsum2  22549  tsmsxp  24130  noinfres  27700  ax5seg  29021  br8d  32696  br8  35954  cgrextend  36206  segconeq  36208  trisegint  36226  ifscgr  36242  cgrsub  36243  btwnxfr  36254  seglecgr12im  36308  segletr  36312  exatleN  39864  atbtwn  39906  3dim1  39927  3dim2  39928  2llnjaN  40026  4atlem10b  40065  4atlem11  40069  4atlem12  40072  2lplnj  40080  cdlemb  40254  paddasslem4  40283  pmodlem1  40306  4atex2  40537  trlval3  40647  arglem1N  40650  cdleme0moN  40685  cdleme17b  40747  cdleme20  40784  cdleme21j  40796  cdleme28c  40832  cdleme35h2  40917  cdleme38n  40924  cdlemg6c  41080  cdlemg6  41083  cdlemg7N  41086  cdlemg11a  41097  cdlemg12e  41107  cdlemg16  41117  cdlemg16ALTN  41118  cdlemg16zz  41120  cdlemg20  41145  cdlemg22  41147  cdlemg37  41149  cdlemg31d  41160  cdlemg29  41165  cdlemg33b  41167  cdlemg33  41171  cdlemg39  41176  cdlemg42  41189  cdlemk25-3  41364