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  27908  noinfres  27923  ax5seglem3a  29317  ax5seg  29325  uhgrwkspth  30141  usgr2wlkspth  30145  br8d  32990  br8  36269  cgrextend  36521  segconeq  36523  trisegint  36541  ifscgr  36557  cgrsub  36558  btwnxfr  36569  seglecgr12im  36623  segletr  36627  atbtwn  40261  3dim1  40282  2llnjaN  40381  4atlem10b  40420  4atlem11  40424  4atlem12  40427  2lplnj  40435  paddasslem4  40638  pmodlem1  40661  4atex2  40892  trlval3  41002  arglem1N  41005  cdleme0moN  41040  cdleme17b  41102  cdleme20  41139  cdleme21j  41151  cdleme28c  41187  cdleme35h2  41272  cdlemg6c  41435  cdlemg6  41438  cdlemg7N  41441  cdlemg8c  41444  cdlemg11a  41452  cdlemg11b  41457  cdlemg12e  41462  cdlemg16  41472  cdlemg16ALTN  41473  cdlemg16zz  41475  cdlemg20  41500  cdlemg22  41502  cdlemg37  41504  cdlemg31d  41515  cdlemg33b  41522  cdlemg33  41526  cdlemg39  41531  cdlemg42  41544  cdlemk25-3  41719  cdlemk33N  41724  cdlemk53b  41771