Theorem simpl31 1253

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpl31	⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

Proof of Theorem simpl31

Step	Hyp	Ref	Expression
1		simpl1 1190	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl3 1186	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3a  27298  ax5seg  27306  uhgrwkspth  28123  usgr2wlkspth  28127  br8d  30950  br8  33723  nosupres  33910  noinfres  33925  cgrextend  34310  segconeq  34312  trisegint  34330  ifscgr  34346  cgrsub  34347  btwnxfr  34358  seglecgr12im  34412  segletr  34416  atbtwn  37460  3dim1  37481  2llnjaN  37580  4atlem10b  37619  4atlem11  37623  4atlem12  37626  2lplnj  37634  paddasslem4  37837  pmodlem1  37860  4atex2  38091  trlval3  38201  arglem1N  38204  cdleme0moN  38239  cdleme17b  38301  cdleme20  38338  cdleme21j  38350  cdleme28c  38386  cdleme35h2  38471  cdlemg6c  38634  cdlemg6  38637  cdlemg7N  38640  cdlemg8c  38643  cdlemg11a  38651  cdlemg11b  38656  cdlemg12e  38661  cdlemg16  38671  cdlemg16ALTN  38672  cdlemg16zz  38674  cdlemg20  38699  cdlemg22  38701  cdlemg37  38703  cdlemg31d  38714  cdlemg33b  38721  cdlemg33  38725  cdlemg39  38730  cdlemg42  38743  cdlemk25-3  38918  cdlemk33N  38923  cdlemk53b  38970