Theorem simpl33 1256

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1089

This theorem is referenced by:  nosupres  27092  noinfres  27107  ax5seglem3a  27942  ax5seg  27950  numclwwlk1lem2foa  29361  br8d  31596  br8  34415  cgrextend  34669  segconeq  34671  trisegint  34689  ifscgr  34705  cgrsub  34706  btwnxfr  34717  seglecgr12im  34771  segletr  34775  atbtwn  37982  4atlem10b  38141  4atlem11  38145  4atlem12  38148  2lplnj  38156  paddasslem4  38359  paddasslem7  38362  pmodlem1  38382  4atex2  38613  trlval3  38723  arglem1N  38726  cdleme0moN  38761  cdleme20  38860  cdleme21j  38872  cdleme28c  38908  cdleme38n  39000  cdlemg6c  39156  cdlemg6  39159  cdlemg7N  39162  cdlemg16  39193  cdlemg16ALTN  39194  cdlemg16zz  39196  cdlemg20  39221  cdlemg22  39223  cdlemg37  39225  cdlemg31d  39236  cdlemg29  39241  cdlemg33b  39243  cdlemg33  39247  cdlemg46  39271  cdlemk25-3  39440