Theorem simpl33 1258

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1089

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 210  df-an 400  df-3an 1091

This theorem is referenced by:  ax5seglem3a  26975  ax5seg  26983  numclwwlk1lem2foa  28391  br8d  30623  br8  33393  nosupres  33596  noinfres  33611  cgrextend  33996  segconeq  33998  trisegint  34016  ifscgr  34032  cgrsub  34033  btwnxfr  34044  seglecgr12im  34098  segletr  34102  atbtwn  37146  4atlem10b  37305  4atlem11  37309  4atlem12  37312  2lplnj  37320  paddasslem4  37523  paddasslem7  37526  pmodlem1  37546  4atex2  37777  trlval3  37887  arglem1N  37890  cdleme0moN  37925  cdleme20  38024  cdleme21j  38036  cdleme28c  38072  cdleme38n  38164  cdlemg6c  38320  cdlemg6  38323  cdlemg7N  38326  cdlemg16  38357  cdlemg16ALTN  38358  cdlemg16zz  38360  cdlemg20  38385  cdlemg22  38387  cdlemg37  38389  cdlemg31d  38400  cdlemg29  38405  cdlemg33b  38407  cdlemg33  38411  cdlemg46  38435  cdlemk25-3  38604