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  27625  noinfres  27640  ax5seglem3a  28863  ax5seg  28871  numclwwlk1lem2foa  30289  br8d  32544  br8  35738  cgrextend  35991  segconeq  35993  trisegint  36011  ifscgr  36027  cgrsub  36028  btwnxfr  36039  seglecgr12im  36093  segletr  36097  atbtwn  39435  4atlem10b  39594  4atlem11  39598  4atlem12  39601  2lplnj  39609  paddasslem4  39812  paddasslem7  39815  pmodlem1  39835  4atex2  40066  trlval3  40176  arglem1N  40179  cdleme0moN  40214  cdleme20  40313  cdleme21j  40325  cdleme28c  40361  cdleme38n  40453  cdlemg6c  40609  cdlemg6  40612  cdlemg7N  40615  cdlemg16  40646  cdlemg16ALTN  40647  cdlemg16zz  40649  cdlemg20  40674  cdlemg22  40676  cdlemg37  40678  cdlemg31d  40689  cdlemg29  40694  cdlemg33b  40696  cdlemg33  40700  cdlemg46  40724  cdlemk25-3  40893