Theorem simprr1 1240

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

Assertion

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

Proof of Theorem simprr1

Step	Hyp	Ref	Expression
1		simp1 1154	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 742	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:  poxp2  8145  sqrmo  15342  icodiamlt  15529  psgnunilem2  19628  haust1  23583  cnhaus  23585  isreg2  23608  llynlly  23709  restnlly  23714  llyrest  23717  llyidm  23720  nllyidm  23721  cldllycmp  23727  txlly  23868  txnlly  23869  pthaus  23870  txhaus  23879  txkgen  23884  xkohaus  23885  xkococnlem  23891  hauspwpwf1  24219  itg2add  25993  ulmdvlem3  26645  nosupno  27947  noinfno  27962  etaslts  28066  cutbdaybnd  28068  cutbdaybnd2  28069  addsproplem6  28247  negsproplem6  28306  mulsproplem13  28401  mulsproplem14  28402  mulsprop  28403  bdayfinbndlem1  28740  ax5seglem6  29399  fusgrfis  29798  umgr2wlkon  30426  numclwwlk5  30876  connpconn  35822  cvmliftmolem2  35869  cvmlift2lem10  35899  cvmlift3lem2  35907  cvmlift3lem8  35913  broutsideof3  36714  unblimceq0  37212  paddasslem10  40710  lhpexle2lem  40890  lhpexle3lem  40892  cdlemj3  41704  cdlemkid4  41815  mpaaeu  43999  stoweidlem35  46871  stoweidlem56  46892  stoweidlem59  46895  2arwcat  50534