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 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  27767  noinfres  27782  ax5seglem3a  28960  ax5seg  28968  uhgrwkspth  29788  usgr2wlkspth  29792  br8d  32630  br8  35736  cgrextend  35990  segconeq  35992  trisegint  36010  ifscgr  36026  cgrsub  36027  btwnxfr  36038  seglecgr12im  36092  segletr  36096  atbtwn  39429  3dim1  39450  2llnjaN  39549  4atlem10b  39588  4atlem11  39592  4atlem12  39595  2lplnj  39603  paddasslem4  39806  pmodlem1  39829  4atex2  40060  trlval3  40170  arglem1N  40173  cdleme0moN  40208  cdleme17b  40270  cdleme20  40307  cdleme21j  40319  cdleme28c  40355  cdleme35h2  40440  cdlemg6c  40603  cdlemg6  40606  cdlemg7N  40609  cdlemg8c  40612  cdlemg11a  40620  cdlemg11b  40625  cdlemg12e  40630  cdlemg16  40640  cdlemg16ALTN  40641  cdlemg16zz  40643  cdlemg20  40668  cdlemg22  40670  cdlemg37  40672  cdlemg31d  40683  cdlemg33b  40690  cdlemg33  40694  cdlemg39  40699  cdlemg42  40712  cdlemk25-3  40887  cdlemk33N  40892  cdlemk53b  40939