Theorem simpl33 1257

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1088

This theorem is referenced by:  nosupres  27671  noinfres  27686  ax5seglem3a  28909  ax5seg  28917  numclwwlk1lem2foa  30335  br8d  32590  br8  35773  cgrextend  36026  segconeq  36028  trisegint  36046  ifscgr  36062  cgrsub  36063  btwnxfr  36074  seglecgr12im  36128  segletr  36132  atbtwn  39465  4atlem10b  39624  4atlem11  39628  4atlem12  39631  2lplnj  39639  paddasslem4  39842  paddasslem7  39845  pmodlem1  39865  4atex2  40096  trlval3  40206  arglem1N  40209  cdleme0moN  40244  cdleme20  40343  cdleme21j  40355  cdleme28c  40391  cdleme38n  40483  cdlemg6c  40639  cdlemg6  40642  cdlemg7N  40645  cdlemg16  40676  cdlemg16ALTN  40677  cdlemg16zz  40679  cdlemg20  40704  cdlemg22  40706  cdlemg37  40708  cdlemg31d  40719  cdlemg29  40724  cdlemg33b  40726  cdlemg33  40730  cdlemg46  40754  cdlemk25-3  40923