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 ⊢ (((𝜃 ∧ 𝜏 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒)) ∧ 𝜂) → 𝜑)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  nosupres  28046  noinfres  28061  ax5seglem3a  29490  ax5seg  29498  uhgrwkspth  30323  usgr2wlkspth  30327  br8d  33184  br8  36490  cgrextend  36743  segconeq  36745  trisegint  36763  ifscgr  36779  cgrsub  36780  btwnxfr  36791  seglecgr12im  36845  segletr  36849  atbtwn  40471  3dim1  40492  2llnjaN  40591  4atlem10b  40630  4atlem11  40634  4atlem12  40637  2lplnj  40645  paddasslem4  40848  pmodlem1  40871  4atex2  41102  trlval3  41212  arglem1N  41215  cdleme0moN  41250  cdleme17b  41312  cdleme20  41349  cdleme21j  41361  cdleme28c  41397  cdleme35h2  41482  cdlemg6c  41645  cdlemg6  41648  cdlemg7N  41651  cdlemg8c  41654  cdlemg11a  41662  cdlemg11b  41667  cdlemg12e  41672  cdlemg16  41682  cdlemg16ALTN  41683  cdlemg16zz  41685  cdlemg20  41710  cdlemg22  41712  cdlemg37  41714  cdlemg31d  41725  cdlemg33b  41732  cdlemg33  41736  cdlemg39  41741  cdlemg42  41754  cdlemk25-3  41929  cdlemk33N  41934  cdlemk53b  41981