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  27649  noinfres  27664  ax5seglem3a  28912  ax5seg  28920  uhgrwkspth  29737  usgr2wlkspth  29741  br8d  32595  br8  35823  cgrextend  36075  segconeq  36077  trisegint  36095  ifscgr  36111  cgrsub  36112  btwnxfr  36123  seglecgr12im  36177  segletr  36181  atbtwn  39568  3dim1  39589  2llnjaN  39688  4atlem10b  39727  4atlem11  39731  4atlem12  39734  2lplnj  39742  paddasslem4  39945  pmodlem1  39968  4atex2  40199  trlval3  40309  arglem1N  40312  cdleme0moN  40347  cdleme17b  40409  cdleme20  40446  cdleme21j  40458  cdleme28c  40494  cdleme35h2  40579  cdlemg6c  40742  cdlemg6  40745  cdlemg7N  40748  cdlemg8c  40751  cdlemg11a  40759  cdlemg11b  40764  cdlemg12e  40769  cdlemg16  40779  cdlemg16ALTN  40780  cdlemg16zz  40782  cdlemg20  40807  cdlemg22  40809  cdlemg37  40811  cdlemg31d  40822  cdlemg33b  40829  cdlemg33  40833  cdlemg39  40838  cdlemg42  40851  cdlemk25-3  41026  cdlemk33N  41031  cdlemk53b  41078