Theorem simpl31 1250

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 399  df-3an 1085

This theorem is referenced by:  ax5seglem3a  26715  ax5seg  26723  uhgrwkspth  27535  usgr2wlkspth  27539  br8d  30360  br8  32992  nosupres  33207  cgrextend  33469  segconeq  33471  trisegint  33489  ifscgr  33505  cgrsub  33506  btwnxfr  33517  seglecgr12im  33571  segletr  33575  atbtwn  36581  3dim1  36602  2llnjaN  36701  4atlem10b  36740  4atlem11  36744  4atlem12  36747  2lplnj  36755  paddasslem4  36958  pmodlem1  36981  4atex2  37212  trlval3  37322  arglem1N  37325  cdleme0moN  37360  cdleme17b  37422  cdleme20  37459  cdleme21j  37471  cdleme28c  37507  cdleme35h2  37592  cdlemg6c  37755  cdlemg6  37758  cdlemg7N  37761  cdlemg8c  37764  cdlemg11a  37772  cdlemg11b  37777  cdlemg12e  37782  cdlemg16  37792  cdlemg16ALTN  37793  cdlemg16zz  37795  cdlemg20  37820  cdlemg22  37822  cdlemg37  37824  cdlemg31d  37835  cdlemg33b  37842  cdlemg33  37846  cdlemg39  37851  cdlemg42  37864  cdlemk25-3  38039  cdlemk33N  38044  cdlemk53b  38091