Theorem simpl33 1257

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

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

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 1088

This theorem is referenced by:  nosupres  27626  noinfres  27641  ax5seglem3a  28864  ax5seg  28872  numclwwlk1lem2foa  30290  br8d  32545  br8  35750  cgrextend  36003  segconeq  36005  trisegint  36023  ifscgr  36039  cgrsub  36040  btwnxfr  36051  seglecgr12im  36105  segletr  36109  atbtwn  39447  4atlem10b  39606  4atlem11  39610  4atlem12  39613  2lplnj  39621  paddasslem4  39824  paddasslem7  39827  pmodlem1  39847  4atex2  40078  trlval3  40188  arglem1N  40191  cdleme0moN  40226  cdleme20  40325  cdleme21j  40337  cdleme28c  40373  cdleme38n  40465  cdlemg6c  40621  cdlemg6  40624  cdlemg7N  40627  cdlemg16  40658  cdlemg16ALTN  40659  cdlemg16zz  40661  cdlemg20  40686  cdlemg22  40688  cdlemg37  40690  cdlemg31d  40701  cdlemg29  40706  cdlemg33b  40708  cdlemg33  40712  cdlemg46  40736  cdlemk25-3  40905