Theorem simpl33 1255

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1086

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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3a  27308  ax5seg  27316  numclwwlk1lem2foa  28726  br8d  30958  br8  33731  nosupres  33918  noinfres  33933  cgrextend  34318  segconeq  34320  trisegint  34338  ifscgr  34354  cgrsub  34355  btwnxfr  34366  seglecgr12im  34420  segletr  34424  atbtwn  37468  4atlem10b  37627  4atlem11  37631  4atlem12  37634  2lplnj  37642  paddasslem4  37845  paddasslem7  37848  pmodlem1  37868  4atex2  38099  trlval3  38209  arglem1N  38212  cdleme0moN  38247  cdleme20  38346  cdleme21j  38358  cdleme28c  38394  cdleme38n  38486  cdlemg6c  38642  cdlemg6  38645  cdlemg7N  38648  cdlemg16  38679  cdlemg16ALTN  38680  cdlemg16zz  38682  cdlemg20  38707  cdlemg22  38709  cdlemg37  38711  cdlemg31d  38722  cdlemg29  38727  cdlemg33b  38729  cdlemg33  38733  cdlemg46  38757  cdlemk25-3  38926