Theorem simpr1l 1227

Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 24-Jun-2022.)

Assertion

Ref	Expression
simpr1l	⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Proof of Theorem simpr1l

Step	Hyp	Ref	Expression
1		simprl 769	. 2 ⊢ ((𝜏 ∧ (𝜑 ∧ 𝜓)) → 𝜑)
2	1	3ad2antr1 1185	1 ⊢ ((𝜏 ∧ ((𝜑 ∧ 𝜓) ∧ 𝜒 ∧ 𝜃)) → 𝜑)

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  poxp2  8146  poxp3  8153  oppccatid  17701  subccatid  17832  setccatid  18073  catccatid  18095  estrccatid  18122  xpccatid  18179  gsmsymgreqlem1  19393  dmdprdsplit  20012  neiptopnei  23073  neitr  23121  neitx  23548  tx1stc  23591  utop3cls  24193  metustsym  24501  ax5seg  28812  clwwlkccat  29863  3pthdlem1  30037  esumpcvgval  33784  esum2d  33799  ifscgr  35727  brofs2  35760  brifs2  35761  btwnconn1lem8  35777  btwnconn1lem12  35781  seglecgr12im  35793  unbdqndv2  36073  lhp2lt  39560  cdlemd1  39757  cdleme3b  39788  cdleme3c  39789  cdleme3e  39791  cdlemf2  40121  cdlemg4c  40171  cdlemn11pre  40769  dihmeetlem12N  40877  stoweidlem60  45528  isthincd2  48172  mndtccatid  48227

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »