Theorem simprr1 1222

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 1136	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜑)
2	1	ad2antll 729	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:  poxp2  8073  sqrmo  15155  icodiamlt  15342  psgnunilem2  19405  haust1  23265  cnhaus  23267  isreg2  23290  llynlly  23390  restnlly  23395  llyrest  23398  llyidm  23401  nllyidm  23402  cldllycmp  23408  txlly  23549  txnlly  23550  pthaus  23551  txhaus  23560  txkgen  23565  xkohaus  23566  xkococnlem  23572  hauspwpwf1  23900  itg2add  25685  ulmdvlem3  26336  nosupno  27640  noinfno  27655  etasslt  27752  scutbdaybnd  27754  scutbdaybnd2  27755  addsproplem6  27915  negsproplem6  27973  mulsproplem13  28065  mulsproplem14  28066  mulsprop  28067  ax5seglem6  28910  fusgrfis  29306  umgr2wlkon  29926  numclwwlk5  30363  connpconn  35267  cvmliftmolem2  35314  cvmlift2lem10  35344  cvmlift3lem2  35352  cvmlift3lem8  35358  broutsideof3  36159  unblimceq0  36540  paddasslem10  39867  lhpexle2lem  40047  lhpexle3lem  40049  cdlemj3  40861  cdlemkid4  40972  mpaaeu  43182  stoweidlem35  46072  stoweidlem56  46093  stoweidlem59  46096  2arwcat  49631