Theorem simpl33 1258

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

Assertion

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

Proof of Theorem simpl33

Step	Hyp	Ref	Expression
1		simpl3 1195	. 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:  nosupres  27685  noinfres  27700  ax5seglem3a  29013  ax5seg  29021  numclwwlk1lem2foa  30439  br8d  32696  br8  35954  cgrextend  36206  segconeq  36208  trisegint  36226  ifscgr  36242  cgrsub  36243  btwnxfr  36254  seglecgr12im  36308  segletr  36312  atbtwn  39906  4atlem10b  40065  4atlem11  40069  4atlem12  40072  2lplnj  40080  paddasslem4  40283  paddasslem7  40286  pmodlem1  40306  4atex2  40537  trlval3  40647  arglem1N  40650  cdleme0moN  40685  cdleme20  40784  cdleme21j  40796  cdleme28c  40832  cdleme38n  40924  cdlemg6c  41080  cdlemg6  41083  cdlemg7N  41086  cdlemg16  41117  cdlemg16ALTN  41118  cdlemg16zz  41120  cdlemg20  41145  cdlemg22  41147  cdlemg37  41149  cdlemg31d  41160  cdlemg29  41165  cdlemg33b  41167  cdlemg33  41171  cdlemg46  41195  cdlemk25-3  41364