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  27687  noinfres  27702  ax5seglem3a  29015  ax5seg  29023  uhgrwkspth  29840  usgr2wlkspth  29844  br8d  32697  br8  35969  cgrextend  36221  segconeq  36223  trisegint  36241  ifscgr  36257  cgrsub  36258  btwnxfr  36269  seglecgr12im  36323  segletr  36327  atbtwn  39819  3dim1  39840  2llnjaN  39939  4atlem10b  39978  4atlem11  39982  4atlem12  39985  2lplnj  39993  paddasslem4  40196  pmodlem1  40219  4atex2  40450  trlval3  40560  arglem1N  40563  cdleme0moN  40598  cdleme17b  40660  cdleme20  40697  cdleme21j  40709  cdleme28c  40745  cdleme35h2  40830  cdlemg6c  40993  cdlemg6  40996  cdlemg7N  40999  cdlemg8c  41002  cdlemg11a  41010  cdlemg11b  41015  cdlemg12e  41020  cdlemg16  41030  cdlemg16ALTN  41031  cdlemg16zz  41033  cdlemg20  41058  cdlemg22  41060  cdlemg37  41062  cdlemg31d  41073  cdlemg33b  41080  cdlemg33  41084  cdlemg39  41089  cdlemg42  41102  cdlemk25-3  41277  cdlemk33N  41282  cdlemk53b  41329