Theorem simpl31 1273

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  27951  noinfres  27966  ax5seglem3a  29395  ax5seg  29403  uhgrwkspth  30228  usgr2wlkspth  30232  br8d  33089  br8  36343  cgrextend  36596  segconeq  36598  trisegint  36616  ifscgr  36632  cgrsub  36633  btwnxfr  36644  seglecgr12im  36698  segletr  36702  atbtwn  40327  3dim1  40348  2llnjaN  40447  4atlem10b  40486  4atlem11  40490  4atlem12  40493  2lplnj  40501  paddasslem4  40704  pmodlem1  40727  4atex2  40958  trlval3  41068  arglem1N  41071  cdleme0moN  41106  cdleme17b  41168  cdleme20  41205  cdleme21j  41217  cdleme28c  41253  cdleme35h2  41338  cdlemg6c  41501  cdlemg6  41504  cdlemg7N  41507  cdlemg8c  41510  cdlemg11a  41518  cdlemg11b  41523  cdlemg12e  41528  cdlemg16  41538  cdlemg16ALTN  41539  cdlemg16zz  41541  cdlemg20  41566  cdlemg22  41568  cdlemg37  41570  cdlemg31d  41581  cdlemg33b  41588  cdlemg33  41592  cdlemg39  41597  cdlemg42  41610  cdlemk25-3  41785  cdlemk33N  41790  cdlemk53b  41837