Theorem simpl31 1325

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

Syntax hints:   → wi 4   ∧ wa 382   ∧ w3a 1070

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 197  df-an 383  df-3an 1072

This theorem is referenced by:  ax5seglem3a  26030  ax5seg  26038  uhgrwkspth  26885  usgr2wlkspth  26889  br8d  29754  br8  31978  nosupres  32184  cgrextend  32446  segconeq  32448  trisegint  32466  ifscgr  32482  cgrsub  32483  btwnxfr  32494  seglecgr12im  32548  segletr  32552  atbtwn  35247  3dim1  35268  2llnjaN  35367  4atlem10b  35406  4atlem11  35410  4atlem12  35413  2lplnj  35421  paddasslem4  35624  pmodlem1  35647  4atex2  35878  trlval3  35989  arglem1N  35992  cdleme0moN  36027  cdleme17b  36089  cdleme20  36126  cdleme21j  36138  cdleme28c  36174  cdleme35h2  36259  cdlemg6c  36422  cdlemg6  36425  cdlemg7N  36428  cdlemg8c  36431  cdlemg11a  36439  cdlemg11b  36444  cdlemg12e  36449  cdlemg16  36459  cdlemg16ALTN  36460  cdlemg16zz  36462  cdlemg20  36487  cdlemg22  36489  cdlemg37  36491  cdlemg31d  36502  cdlemg33b  36509  cdlemg33  36513  cdlemg39  36518  cdlemg42  36531  cdlemk25-3  36706  cdlemk33N  36711  cdlemk53b  36758