Theorem simpl33 1264

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1093

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 209  df-an 398  df-3an 1095

This theorem is referenced by:  nosupres  27693  noinfres  27708  ax5seglem3a  29021  ax5seg  29029  numclwwlk1lem2foa  30446  br8d  32704  br8  35999  cgrextend  36251  segconeq  36253  trisegint  36271  ifscgr  36287  cgrsub  36288  btwnxfr  36299  seglecgr12im  36353  segletr  36357  atbtwn  39953  4atlem10b  40112  4atlem11  40116  4atlem12  40119  2lplnj  40127  paddasslem4  40330  paddasslem7  40333  pmodlem1  40353  4atex2  40584  trlval3  40694  arglem1N  40697  cdleme0moN  40732  cdleme20  40831  cdleme21j  40843  cdleme28c  40879  cdleme38n  40971  cdlemg6c  41127  cdlemg6  41130  cdlemg7N  41133  cdlemg16  41164  cdlemg16ALTN  41165  cdlemg16zz  41167  cdlemg20  41192  cdlemg22  41194  cdlemg37  41196  cdlemg31d  41207  cdlemg29  41212  cdlemg33b  41214  cdlemg33  41218  cdlemg46  41242  cdlemk25-3  41411