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  28097  noinfres  28112  ax5seglem3a  29541  ax5seg  29549  numclwwlk1lem2foa  30988  br8d  33277  br8  36712  cgrextend  36964  segconeq  36966  trisegint  36984  ifscgr  37000  cgrsub  37001  btwnxfr  37012  seglecgr12im  37066  segletr  37070  atbtwn  40706  4atlem10b  40865  4atlem11  40869  4atlem12  40872  2lplnj  40880  paddasslem4  41083  paddasslem7  41086  pmodlem1  41106  4atex2  41337  trlval3  41447  arglem1N  41450  cdleme0moN  41485  cdleme20  41584  cdleme21j  41596  cdleme28c  41632  cdleme38n  41724  cdlemg6c  41880  cdlemg6  41883  cdlemg7N  41886  cdlemg16  41917  cdlemg16ALTN  41918  cdlemg16zz  41920  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg31d  41960  cdlemg29  41965  cdlemg33b  41967  cdlemg33  41971  cdlemg46  41995  cdlemk25-3  42164