Theorem simpl31 1273

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1103

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 401  df-3an 1105

This theorem is referenced by:  nosupres  27852  noinfres  27867  ax5seglem3a  29261  ax5seg  29269  uhgrwkspth  30085  usgr2wlkspth  30089  br8d  32934  br8  36229  cgrextend  36481  segconeq  36483  trisegint  36501  ifscgr  36517  cgrsub  36518  btwnxfr  36529  seglecgr12im  36583  segletr  36587  atbtwn  40201  3dim1  40222  2llnjaN  40321  4atlem10b  40360  4atlem11  40364  4atlem12  40367  2lplnj  40375  paddasslem4  40578  pmodlem1  40601  4atex2  40832  trlval3  40942  arglem1N  40945  cdleme0moN  40980  cdleme17b  41042  cdleme20  41079  cdleme21j  41091  cdleme28c  41127  cdleme35h2  41212  cdlemg6c  41375  cdlemg6  41378  cdlemg7N  41381  cdlemg8c  41384  cdlemg11a  41392  cdlemg11b  41397  cdlemg12e  41402  cdlemg16  41412  cdlemg16ALTN  41413  cdlemg16zz  41415  cdlemg20  41440  cdlemg22  41442  cdlemg37  41444  cdlemg31d  41455  cdlemg33b  41462  cdlemg33  41466  cdlemg39  41471  cdlemg42  41484  cdlemk25-3  41659  cdlemk33N  41664  cdlemk53b  41711