Theorem simpl31 1256

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

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

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 1089

This theorem is referenced by:  nosupres  27671  noinfres  27686  ax5seglem3a  28999  ax5seg  29007  uhgrwkspth  29823  usgr2wlkspth  29827  br8d  32681  br8  35938  cgrextend  36190  segconeq  36192  trisegint  36210  ifscgr  36226  cgrsub  36227  btwnxfr  36238  seglecgr12im  36292  segletr  36296  atbtwn  39892  3dim1  39913  2llnjaN  40012  4atlem10b  40051  4atlem11  40055  4atlem12  40058  2lplnj  40066  paddasslem4  40269  pmodlem1  40292  4atex2  40523  trlval3  40633  arglem1N  40636  cdleme0moN  40671  cdleme17b  40733  cdleme20  40770  cdleme21j  40782  cdleme28c  40818  cdleme35h2  40903  cdlemg6c  41066  cdlemg6  41069  cdlemg7N  41072  cdlemg8c  41075  cdlemg11a  41083  cdlemg11b  41088  cdlemg12e  41093  cdlemg16  41103  cdlemg16ALTN  41104  cdlemg16zz  41106  cdlemg20  41131  cdlemg22  41133  cdlemg37  41135  cdlemg31d  41146  cdlemg33b  41153  cdlemg33  41157  cdlemg39  41162  cdlemg42  41175  cdlemk25-3  41350  cdlemk33N  41355  cdlemk53b  41402