Theorem simpl31 1251

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

Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084

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 210  df-an 400  df-3an 1086

This theorem is referenced by:  ax5seglem3a  26724  ax5seg  26732  uhgrwkspth  27544  usgr2wlkspth  27548  br8d  30374  br8  33105  nosupres  33320  cgrextend  33582  segconeq  33584  trisegint  33602  ifscgr  33618  cgrsub  33619  btwnxfr  33630  seglecgr12im  33684  segletr  33688  atbtwn  36742  3dim1  36763  2llnjaN  36862  4atlem10b  36901  4atlem11  36905  4atlem12  36908  2lplnj  36916  paddasslem4  37119  pmodlem1  37142  4atex2  37373  trlval3  37483  arglem1N  37486  cdleme0moN  37521  cdleme17b  37583  cdleme20  37620  cdleme21j  37632  cdleme28c  37668  cdleme35h2  37753  cdlemg6c  37916  cdlemg6  37919  cdlemg7N  37922  cdlemg8c  37925  cdlemg11a  37933  cdlemg11b  37938  cdlemg12e  37943  cdlemg16  37953  cdlemg16ALTN  37954  cdlemg16zz  37956  cdlemg20  37981  cdlemg22  37983  cdlemg37  37985  cdlemg31d  37996  cdlemg33b  38003  cdlemg33  38007  cdlemg39  38012  cdlemg42  38025  cdlemk25-3  38200  cdlemk33N  38205  cdlemk53b  38252