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 394   ∧ 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 395  df-3an 1087

This theorem is referenced by:  nosupres  27446  noinfres  27461  ax5seglem3a  28455  ax5seg  28463  uhgrwkspth  29279  usgr2wlkspth  29283  br8d  32106  br8  35030  cgrextend  35284  segconeq  35286  trisegint  35304  ifscgr  35320  cgrsub  35321  btwnxfr  35332  seglecgr12im  35386  segletr  35390  atbtwn  38620  3dim1  38641  2llnjaN  38740  4atlem10b  38779  4atlem11  38783  4atlem12  38786  2lplnj  38794  paddasslem4  38997  pmodlem1  39020  4atex2  39251  trlval3  39361  arglem1N  39364  cdleme0moN  39399  cdleme17b  39461  cdleme20  39498  cdleme21j  39510  cdleme28c  39546  cdleme35h2  39631  cdlemg6c  39794  cdlemg6  39797  cdlemg7N  39800  cdlemg8c  39803  cdlemg11a  39811  cdlemg11b  39816  cdlemg12e  39821  cdlemg16  39831  cdlemg16ALTN  39832  cdlemg16zz  39834  cdlemg20  39859  cdlemg22  39861  cdlemg37  39863  cdlemg31d  39874  cdlemg33b  39881  cdlemg33  39885  cdlemg39  39890  cdlemg42  39903  cdlemk25-3  40078  cdlemk33N  40083  cdlemk53b  40130