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  28064  noinfres  28079  ax5seglem3a  29508  ax5seg  29516  uhgrwkspth  30341  usgr2wlkspth  30345  br8d  33202  br8  36521  cgrextend  36773  segconeq  36775  trisegint  36793  ifscgr  36809  cgrsub  36810  btwnxfr  36821  seglecgr12im  36875  segletr  36879  atbtwn  40504  3dim1  40525  2llnjaN  40624  4atlem10b  40663  4atlem11  40667  4atlem12  40670  2lplnj  40678  paddasslem4  40881  pmodlem1  40904  4atex2  41135  trlval3  41245  arglem1N  41248  cdleme0moN  41283  cdleme17b  41345  cdleme20  41382  cdleme21j  41394  cdleme28c  41430  cdleme35h2  41515  cdlemg6c  41678  cdlemg6  41681  cdlemg7N  41684  cdlemg8c  41687  cdlemg11a  41695  cdlemg11b  41700  cdlemg12e  41705  cdlemg16  41715  cdlemg16ALTN  41716  cdlemg16zz  41718  cdlemg20  41743  cdlemg22  41745  cdlemg37  41747  cdlemg31d  41758  cdlemg33b  41765  cdlemg33  41769  cdlemg39  41774  cdlemg42  41787  cdlemk25-3  41962  cdlemk33N  41967  cdlemk53b  42014