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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  28046  noinfres  28061  ax5seglem3a  29490  ax5seg  29498  numclwwlk1lem2foa  30937  br8d  33184  br8  36490  cgrextend  36743  segconeq  36745  trisegint  36763  ifscgr  36779  cgrsub  36780  btwnxfr  36791  seglecgr12im  36845  segletr  36849  atbtwn  40471  4atlem10b  40630  4atlem11  40634  4atlem12  40637  2lplnj  40645  paddasslem4  40848  paddasslem7  40851  pmodlem1  40871  4atex2  41102  trlval3  41212  arglem1N  41215  cdleme0moN  41250  cdleme20  41349  cdleme21j  41361  cdleme28c  41397  cdleme38n  41489  cdlemg6c  41645  cdlemg6  41648  cdlemg7N  41651  cdlemg16  41682  cdlemg16ALTN  41683  cdlemg16zz  41685  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg31d  41725  cdlemg29  41730  cdlemg33b  41732  cdlemg33  41736  cdlemg46  41760  cdlemk25-3  41929