Theorem simpl31 1255

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 1088

This theorem is referenced by:  nosupres  27635  noinfres  27650  ax5seglem3a  28893  ax5seg  28901  uhgrwkspth  29718  usgr2wlkspth  29722  br8d  32571  br8  35731  cgrextend  35984  segconeq  35986  trisegint  36004  ifscgr  36020  cgrsub  36021  btwnxfr  36032  seglecgr12im  36086  segletr  36090  atbtwn  39428  3dim1  39449  2llnjaN  39548  4atlem10b  39587  4atlem11  39591  4atlem12  39594  2lplnj  39602  paddasslem4  39805  pmodlem1  39828  4atex2  40059  trlval3  40169  arglem1N  40172  cdleme0moN  40207  cdleme17b  40269  cdleme20  40306  cdleme21j  40318  cdleme28c  40354  cdleme35h2  40439  cdlemg6c  40602  cdlemg6  40605  cdlemg7N  40608  cdlemg8c  40611  cdlemg11a  40619  cdlemg11b  40624  cdlemg12e  40629  cdlemg16  40639  cdlemg16ALTN  40640  cdlemg16zz  40642  cdlemg20  40667  cdlemg22  40669  cdlemg37  40671  cdlemg31d  40682  cdlemg33b  40689  cdlemg33  40693  cdlemg39  40698  cdlemg42  40711  cdlemk25-3  40886  cdlemk33N  40891  cdlemk53b  40938