Theorem simpl31 1298

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 1199	. 2 ⊢ (((𝜑 ∧ 𝜓 ∧ 𝜒) ∧ 𝜂) → 𝜑)
2	1	3ad2antl3 1195	1 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 386   ∧ w3a 1071

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 199  df-an 387  df-3an 1073

This theorem is referenced by:  ax5seglem3a  26279  ax5seg  26287  uhgrwkspth  27107  usgr2wlkspth  27111  br8d  29985  br8  32240  nosupres  32442  cgrextend  32704  segconeq  32706  trisegint  32724  ifscgr  32740  cgrsub  32741  btwnxfr  32752  seglecgr12im  32806  segletr  32810  atbtwn  35600  3dim1  35621  2llnjaN  35720  4atlem10b  35759  4atlem11  35763  4atlem12  35766  2lplnj  35774  paddasslem4  35977  pmodlem1  36000  4atex2  36231  trlval3  36341  arglem1N  36344  cdleme0moN  36379  cdleme17b  36441  cdleme20  36478  cdleme21j  36490  cdleme28c  36526  cdleme35h2  36611  cdlemg6c  36774  cdlemg6  36777  cdlemg7N  36780  cdlemg8c  36783  cdlemg11a  36791  cdlemg11b  36796  cdlemg12e  36801  cdlemg16  36811  cdlemg16ALTN  36812  cdlemg16zz  36814  cdlemg20  36839  cdlemg22  36841  cdlemg37  36843  cdlemg31d  36854  cdlemg33b  36861  cdlemg33  36865  cdlemg39  36870  cdlemg42  36883  cdlemk25-3  37058  cdlemk33N  37063  cdlemk53b  37110