Theorem simpl31 1252

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1085

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 396  df-3an 1087

This theorem is referenced by:  ax5seglem3a  27201  ax5seg  27209  uhgrwkspth  28024  usgr2wlkspth  28028  br8d  30851  br8  33629  nosupres  33837  noinfres  33852  cgrextend  34237  segconeq  34239  trisegint  34257  ifscgr  34273  cgrsub  34274  btwnxfr  34285  seglecgr12im  34339  segletr  34343  atbtwn  37387  3dim1  37408  2llnjaN  37507  4atlem10b  37546  4atlem11  37550  4atlem12  37553  2lplnj  37561  paddasslem4  37764  pmodlem1  37787  4atex2  38018  trlval3  38128  arglem1N  38131  cdleme0moN  38166  cdleme17b  38228  cdleme20  38265  cdleme21j  38277  cdleme28c  38313  cdleme35h2  38398  cdlemg6c  38561  cdlemg6  38564  cdlemg7N  38567  cdlemg8c  38570  cdlemg11a  38578  cdlemg11b  38583  cdlemg12e  38588  cdlemg16  38598  cdlemg16ALTN  38599  cdlemg16zz  38601  cdlemg20  38626  cdlemg22  38628  cdlemg37  38630  cdlemg31d  38641  cdlemg33b  38648  cdlemg33  38652  cdlemg39  38657  cdlemg42  38670  cdlemk25-3  38845  cdlemk33N  38850  cdlemk53b  38897