Theorem simpl31 1253

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

Syntax hints:   → wi 4   ∧ wa 396   ∧ 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 206  df-an 397  df-3an 1088

This theorem is referenced by:  ax5seglem3a  27286  ax5seg  27294  uhgrwkspth  28109  usgr2wlkspth  28113  br8d  30936  br8  33709  nosupres  33896  noinfres  33911  cgrextend  34296  segconeq  34298  trisegint  34316  ifscgr  34332  cgrsub  34333  btwnxfr  34344  seglecgr12im  34398  segletr  34402  atbtwn  37446  3dim1  37467  2llnjaN  37566  4atlem10b  37605  4atlem11  37609  4atlem12  37612  2lplnj  37620  paddasslem4  37823  pmodlem1  37846  4atex2  38077  trlval3  38187  arglem1N  38190  cdleme0moN  38225  cdleme17b  38287  cdleme20  38324  cdleme21j  38336  cdleme28c  38372  cdleme35h2  38457  cdlemg6c  38620  cdlemg6  38623  cdlemg7N  38626  cdlemg8c  38629  cdlemg11a  38637  cdlemg11b  38642  cdlemg12e  38647  cdlemg16  38657  cdlemg16ALTN  38658  cdlemg16zz  38660  cdlemg20  38685  cdlemg22  38687  cdlemg37  38689  cdlemg31d  38700  cdlemg33b  38707  cdlemg33  38711  cdlemg39  38716  cdlemg42  38729  cdlemk25-3  38904  cdlemk33N  38909  cdlemk53b  38956