Theorem simpl33 1263

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  nosupres  27696  noinfres  27711  ax5seglem3a  29024  ax5seg  29032  numclwwlk1lem2foa  30449  br8d  32707  br8  35991  cgrextend  36243  segconeq  36245  trisegint  36263  ifscgr  36279  cgrsub  36280  btwnxfr  36291  seglecgr12im  36345  segletr  36349  atbtwn  39945  4atlem10b  40104  4atlem11  40108  4atlem12  40111  2lplnj  40119  paddasslem4  40322  paddasslem7  40325  pmodlem1  40345  4atex2  40576  trlval3  40686  arglem1N  40689  cdleme0moN  40724  cdleme20  40823  cdleme21j  40835  cdleme28c  40871  cdleme38n  40963  cdlemg6c  41119  cdlemg6  41122  cdlemg7N  41125  cdlemg16  41156  cdlemg16ALTN  41157  cdlemg16zz  41159  cdlemg20  41184  cdlemg22  41186  cdlemg37  41188  cdlemg31d  41199  cdlemg29  41204  cdlemg33b  41206  cdlemg33  41210  cdlemg46  41234  cdlemk25-3  41403