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 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜒)

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

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 1105

This theorem is referenced by:  nosupres  27852  noinfres  27867  ax5seglem3a  29261  ax5seg  29269  numclwwlk1lem2foa  30686  br8d  32934  br8  36229  cgrextend  36481  segconeq  36483  trisegint  36501  ifscgr  36517  cgrsub  36518  btwnxfr  36529  seglecgr12im  36583  segletr  36587  atbtwn  40201  4atlem10b  40360  4atlem11  40364  4atlem12  40367  2lplnj  40375  paddasslem4  40578  paddasslem7  40581  pmodlem1  40601  4atex2  40832  trlval3  40942  arglem1N  40945  cdleme0moN  40980  cdleme20  41079  cdleme21j  41091  cdleme28c  41127  cdleme38n  41219  cdlemg6c  41375  cdlemg6  41378  cdlemg7N  41381  cdlemg16  41412  cdlemg16ALTN  41413  cdlemg16zz  41415  cdlemg20  41440  cdlemg22  41442  cdlemg37  41444  cdlemg31d  41455  cdlemg29  41460  cdlemg33b  41462  cdlemg33  41466  cdlemg46  41490  cdlemk25-3  41659