Theorem simpl31 1255

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

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

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 1088

This theorem is referenced by:  nosupres  27676  noinfres  27691  ax5seglem3a  28914  ax5seg  28922  uhgrwkspth  29742  usgr2wlkspth  29746  br8d  32595  br8  35778  cgrextend  36031  segconeq  36033  trisegint  36051  ifscgr  36067  cgrsub  36068  btwnxfr  36079  seglecgr12im  36133  segletr  36137  atbtwn  39470  3dim1  39491  2llnjaN  39590  4atlem10b  39629  4atlem11  39633  4atlem12  39636  2lplnj  39644  paddasslem4  39847  pmodlem1  39870  4atex2  40101  trlval3  40211  arglem1N  40214  cdleme0moN  40249  cdleme17b  40311  cdleme20  40348  cdleme21j  40360  cdleme28c  40396  cdleme35h2  40481  cdlemg6c  40644  cdlemg6  40647  cdlemg7N  40650  cdlemg8c  40653  cdlemg11a  40661  cdlemg11b  40666  cdlemg12e  40671  cdlemg16  40681  cdlemg16ALTN  40682  cdlemg16zz  40684  cdlemg20  40709  cdlemg22  40711  cdlemg37  40713  cdlemg31d  40724  cdlemg33b  40731  cdlemg33  40735  cdlemg39  40740  cdlemg42  40753  cdlemk25-3  40928  cdlemk33N  40933  cdlemk53b  40980