Theorem simpl33 1273

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  nosupres  27825  noinfres  27840  ax5seglem3a  29185  ax5seg  29193  numclwwlk1lem2foa  30610  br8d  32861  br8  36114  cgrextend  36366  segconeq  36368  trisegint  36386  ifscgr  36402  cgrsub  36403  btwnxfr  36414  seglecgr12im  36468  segletr  36472  atbtwn  40077  4atlem10b  40236  4atlem11  40240  4atlem12  40243  2lplnj  40251  paddasslem4  40454  paddasslem7  40457  pmodlem1  40477  4atex2  40708  trlval3  40818  arglem1N  40821  cdleme0moN  40856  cdleme20  40955  cdleme21j  40967  cdleme28c  41003  cdleme38n  41095  cdlemg6c  41251  cdlemg6  41254  cdlemg7N  41257  cdlemg16  41288  cdlemg16ALTN  41289  cdlemg16zz  41291  cdlemg20  41316  cdlemg22  41318  cdlemg37  41320  cdlemg31d  41331  cdlemg29  41336  cdlemg33b  41338  cdlemg33  41342  cdlemg46  41366  cdlemk25-3  41535