Theorem simpl31 1255

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 1192	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl3 1188	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  27656  noinfres  27671  ax5seglem3a  28919  ax5seg  28927  uhgrwkspth  29744  usgr2wlkspth  29748  br8d  32602  br8  35811  cgrextend  36063  segconeq  36065  trisegint  36083  ifscgr  36099  cgrsub  36100  btwnxfr  36111  seglecgr12im  36165  segletr  36169  atbtwn  39555  3dim1  39576  2llnjaN  39675  4atlem10b  39714  4atlem11  39718  4atlem12  39721  2lplnj  39729  paddasslem4  39932  pmodlem1  39955  4atex2  40186  trlval3  40296  arglem1N  40299  cdleme0moN  40334  cdleme17b  40396  cdleme20  40433  cdleme21j  40445  cdleme28c  40481  cdleme35h2  40566  cdlemg6c  40729  cdlemg6  40732  cdlemg7N  40735  cdlemg8c  40738  cdlemg11a  40746  cdlemg11b  40751  cdlemg12e  40756  cdlemg16  40766  cdlemg16ALTN  40767  cdlemg16zz  40769  cdlemg20  40794  cdlemg22  40796  cdlemg37  40798  cdlemg31d  40809  cdlemg33b  40816  cdlemg33  40820  cdlemg39  40825  cdlemg42  40838  cdlemk25-3  41013  cdlemk33N  41018  cdlemk53b  41065