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  28069  noinfres  28084  ax5seglem3a  29513  ax5seg  29521  uhgrwkspth  30346  usgr2wlkspth  30350  br8d  33249  br8  36613  cgrextend  36865  segconeq  36867  trisegint  36885  ifscgr  36901  cgrsub  36902  btwnxfr  36913  seglecgr12im  36967  segletr  36971  atbtwn  40596  3dim1  40617  2llnjaN  40716  4atlem10b  40755  4atlem11  40759  4atlem12  40762  2lplnj  40770  paddasslem4  40973  pmodlem1  40996  4atex2  41227  trlval3  41337  arglem1N  41340  cdleme0moN  41375  cdleme17b  41437  cdleme20  41474  cdleme21j  41486  cdleme28c  41522  cdleme35h2  41607  cdlemg6c  41770  cdlemg6  41773  cdlemg7N  41776  cdlemg8c  41779  cdlemg11a  41787  cdlemg11b  41792  cdlemg12e  41797  cdlemg16  41807  cdlemg16ALTN  41808  cdlemg16zz  41810  cdlemg20  41835  cdlemg22  41837  cdlemg37  41839  cdlemg31d  41850  cdlemg33b  41857  cdlemg33  41861  cdlemg39  41866  cdlemg42  41879  cdlemk25-3  42054  cdlemk33N  42059  cdlemk53b  42106