Theorem simpl31 1273

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  28097  noinfres  28112  ax5seglem3a  29541  ax5seg  29549  uhgrwkspth  30374  usgr2wlkspth  30378  br8d  33277  br8  36712  cgrextend  36964  segconeq  36966  trisegint  36984  ifscgr  37000  cgrsub  37001  btwnxfr  37012  seglecgr12im  37066  segletr  37070  atbtwn  40706  3dim1  40727  2llnjaN  40826  4atlem10b  40865  4atlem11  40869  4atlem12  40872  2lplnj  40880  paddasslem4  41083  pmodlem1  41106  4atex2  41337  trlval3  41447  arglem1N  41450  cdleme0moN  41485  cdleme17b  41547  cdleme20  41584  cdleme21j  41596  cdleme28c  41632  cdleme35h2  41717  cdlemg6c  41880  cdlemg6  41883  cdlemg7N  41886  cdlemg8c  41889  cdlemg11a  41897  cdlemg11b  41902  cdlemg12e  41907  cdlemg16  41917  cdlemg16ALTN  41918  cdlemg16zz  41920  cdlemg20  41945  cdlemg22  41947  cdlemg37  41949  cdlemg31d  41960  cdlemg33b  41967  cdlemg33  41971  cdlemg39  41976  cdlemg42  41989  cdlemk25-3  42164  cdlemk33N  42169  cdlemk53b  42216