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  28070  noinfres  28085  ax5seglem3a  29514  ax5seg  29522  numclwwlk1lem2foa  30961  br8d  33250  br8  36614  cgrextend  36866  segconeq  36868  trisegint  36886  ifscgr  36902  cgrsub  36903  btwnxfr  36914  seglecgr12im  36968  segletr  36972  atbtwn  40597  4atlem10b  40756  4atlem11  40760  4atlem12  40763  2lplnj  40771  paddasslem4  40974  paddasslem7  40977  pmodlem1  40997  4atex2  41228  trlval3  41338  arglem1N  41341  cdleme0moN  41376  cdleme20  41475  cdleme21j  41487  cdleme28c  41523  cdleme38n  41615  cdlemg6c  41771  cdlemg6  41774  cdlemg7N  41777  cdlemg16  41808  cdlemg16ALTN  41809  cdlemg16zz  41811  cdlemg20  41836  cdlemg22  41838  cdlemg37  41840  cdlemg31d  41851  cdlemg29  41856  cdlemg33b  41858  cdlemg33  41862  cdlemg46  41886  cdlemk25-3  42055