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  27685  noinfres  27700  ax5seglem3a  29013  ax5seg  29021  uhgrwkspth  29838  usgr2wlkspth  29842  br8d  32696  br8  35954  cgrextend  36206  segconeq  36208  trisegint  36226  ifscgr  36242  cgrsub  36243  btwnxfr  36254  seglecgr12im  36308  segletr  36312  atbtwn  39906  3dim1  39927  2llnjaN  40026  4atlem10b  40065  4atlem11  40069  4atlem12  40072  2lplnj  40080  paddasslem4  40283  pmodlem1  40306  4atex2  40537  trlval3  40647  arglem1N  40650  cdleme0moN  40685  cdleme17b  40747  cdleme20  40784  cdleme21j  40796  cdleme28c  40832  cdleme35h2  40917  cdlemg6c  41080  cdlemg6  41083  cdlemg7N  41086  cdlemg8c  41089  cdlemg11a  41097  cdlemg11b  41102  cdlemg12e  41107  cdlemg16  41117  cdlemg16ALTN  41118  cdlemg16zz  41120  cdlemg20  41145  cdlemg22  41147  cdlemg37  41149  cdlemg31d  41160  cdlemg33b  41167  cdlemg33  41171  cdlemg39  41176  cdlemg42  41189  cdlemk25-3  41364  cdlemk33N  41369  cdlemk53b  41416