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  27647  noinfres  27662  ax5seglem3a  28909  ax5seg  28917  uhgrwkspth  29734  usgr2wlkspth  29738  br8d  32589  br8  35798  cgrextend  36048  segconeq  36050  trisegint  36068  ifscgr  36084  cgrsub  36085  btwnxfr  36096  seglecgr12im  36150  segletr  36154  atbtwn  39491  3dim1  39512  2llnjaN  39611  4atlem10b  39650  4atlem11  39654  4atlem12  39657  2lplnj  39665  paddasslem4  39868  pmodlem1  39891  4atex2  40122  trlval3  40232  arglem1N  40235  cdleme0moN  40270  cdleme17b  40332  cdleme20  40369  cdleme21j  40381  cdleme28c  40417  cdleme35h2  40502  cdlemg6c  40665  cdlemg6  40668  cdlemg7N  40671  cdlemg8c  40674  cdlemg11a  40682  cdlemg11b  40687  cdlemg12e  40692  cdlemg16  40702  cdlemg16ALTN  40703  cdlemg16zz  40705  cdlemg20  40730  cdlemg22  40732  cdlemg37  40734  cdlemg31d  40745  cdlemg33b  40752  cdlemg33  40756  cdlemg39  40761  cdlemg42  40774  cdlemk25-3  40949  cdlemk33N  40954  cdlemk53b  41001