Theorem simpl31 1327

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

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072

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 385  df-3an 1074

This theorem is referenced by:  ax5seglem3a  26009  ax5seg  26017  uhgrwkspth  26861  usgr2wlkspth  26865  br8d  29729  br8  31953  nosupres  32159  cgrextend  32421  segconeq  32423  trisegint  32441  ifscgr  32457  cgrsub  32458  btwnxfr  32469  seglecgr12im  32523  segletr  32527  atbtwn  35235  3dim1  35256  2llnjaN  35355  4atlem10b  35394  4atlem11  35398  4atlem12  35401  2lplnj  35409  paddasslem4  35612  pmodlem1  35635  4atex2  35866  trlval3  35977  arglem1N  35980  cdleme0moN  36015  cdleme17b  36077  cdleme20  36114  cdleme21j  36126  cdleme28c  36162  cdleme35h2  36247  cdlemg6c  36410  cdlemg6  36413  cdlemg7N  36416  cdlemg8c  36419  cdlemg11a  36427  cdlemg11b  36432  cdlemg12e  36437  cdlemg16  36447  cdlemg16ALTN  36448  cdlemg16zz  36450  cdlemg20  36475  cdlemg22  36477  cdlemg37  36479  cdlemg31d  36490  cdlemg33b  36497  cdlemg33  36501  cdlemg39  36506  cdlemg42  36519  cdlemk25-3  36694  cdlemk33N  36699  cdlemk53b  36746