Theorem simpl31 1267

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1097

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 209  df-an 400  df-3an 1099

This theorem is referenced by:  nosupres  27758  noinfres  27773  ax5seglem3a  29087  ax5seg  29095  uhgrwkspth  29911  usgr2wlkspth  29915  br8d  32770  br8  36066  cgrextend  36318  segconeq  36320  trisegint  36338  ifscgr  36354  cgrsub  36355  btwnxfr  36366  seglecgr12im  36420  segletr  36424  atbtwn  40030  3dim1  40051  2llnjaN  40150  4atlem10b  40189  4atlem11  40193  4atlem12  40196  2lplnj  40204  paddasslem4  40407  pmodlem1  40430  4atex2  40661  trlval3  40771  arglem1N  40774  cdleme0moN  40809  cdleme17b  40871  cdleme20  40908  cdleme21j  40920  cdleme28c  40956  cdleme35h2  41041  cdlemg6c  41204  cdlemg6  41207  cdlemg7N  41210  cdlemg8c  41213  cdlemg11a  41221  cdlemg11b  41226  cdlemg12e  41231  cdlemg16  41241  cdlemg16ALTN  41242  cdlemg16zz  41244  cdlemg20  41269  cdlemg22  41271  cdlemg37  41273  cdlemg31d  41284  cdlemg33b  41291  cdlemg33  41295  cdlemg39  41300  cdlemg42  41313  cdlemk25-3  41488  cdlemk33N  41493  cdlemk53b  41540