Theorem simpl31 1271

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  nosupres  27825  noinfres  27840  ax5seglem3a  29185  ax5seg  29193  uhgrwkspth  30009  usgr2wlkspth  30013  br8d  32861  br8  36114  cgrextend  36366  segconeq  36368  trisegint  36386  ifscgr  36402  cgrsub  36403  btwnxfr  36414  seglecgr12im  36468  segletr  36472  atbtwn  40077  3dim1  40098  2llnjaN  40197  4atlem10b  40236  4atlem11  40240  4atlem12  40243  2lplnj  40251  paddasslem4  40454  pmodlem1  40477  4atex2  40708  trlval3  40818  arglem1N  40821  cdleme0moN  40856  cdleme17b  40918  cdleme20  40955  cdleme21j  40967  cdleme28c  41003  cdleme35h2  41088  cdlemg6c  41251  cdlemg6  41254  cdlemg7N  41257  cdlemg8c  41260  cdlemg11a  41268  cdlemg11b  41273  cdlemg12e  41278  cdlemg16  41288  cdlemg16ALTN  41289  cdlemg16zz  41291  cdlemg20  41316  cdlemg22  41318  cdlemg37  41320  cdlemg31d  41331  cdlemg33b  41338  cdlemg33  41342  cdlemg39  41347  cdlemg42  41360  cdlemk25-3  41535  cdlemk33N  41540  cdlemk53b  41587