Theorem simpl33 1275

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  27951  noinfres  27966  ax5seglem3a  29395  ax5seg  29403  numclwwlk1lem2foa  30842  br8d  33089  br8  36343  cgrextend  36596  segconeq  36598  trisegint  36616  ifscgr  36632  cgrsub  36633  btwnxfr  36644  seglecgr12im  36698  segletr  36702  atbtwn  40327  4atlem10b  40486  4atlem11  40490  4atlem12  40493  2lplnj  40501  paddasslem4  40704  paddasslem7  40707  pmodlem1  40727  4atex2  40958  trlval3  41068  arglem1N  41071  cdleme0moN  41106  cdleme20  41205  cdleme21j  41217  cdleme28c  41253  cdleme38n  41345  cdlemg6c  41501  cdlemg6  41504  cdlemg7N  41507  cdlemg16  41538  cdlemg16ALTN  41539  cdlemg16zz  41541  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg29  41586  cdlemg33b  41588  cdlemg33  41592  cdlemg46  41616  cdlemk25-3  41785