Theorem simpl33 1256

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  nosupres  27770  noinfres  27785  ax5seglem3a  28963  ax5seg  28971  numclwwlk1lem2foa  30386  br8d  32632  br8  35718  cgrextend  35972  segconeq  35974  trisegint  35992  ifscgr  36008  cgrsub  36009  btwnxfr  36020  seglecgr12im  36074  segletr  36078  atbtwn  39403  4atlem10b  39562  4atlem11  39566  4atlem12  39569  2lplnj  39577  paddasslem4  39780  paddasslem7  39783  pmodlem1  39803  4atex2  40034  trlval3  40144  arglem1N  40147  cdleme0moN  40182  cdleme20  40281  cdleme21j  40293  cdleme28c  40329  cdleme38n  40421  cdlemg6c  40577  cdlemg6  40580  cdlemg7N  40583  cdlemg16  40614  cdlemg16ALTN  40615  cdlemg16zz  40617  cdlemg20  40642  cdlemg22  40644  cdlemg37  40646  cdlemg31d  40657  cdlemg29  40662  cdlemg33b  40664  cdlemg33  40668  cdlemg46  40692  cdlemk25-3  40861