Theorem simprr3 1233

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

Assertion

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

Proof of Theorem simprr3

Step	Hyp	Ref	Expression
1		simp3 1147	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 737	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1095

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 209  df-an 399  df-3an 1097

This theorem is referenced by:  el2xptp0  8006  poxp2  8111  ttrcltr  9661  icodiamlt  15441  psgnunilem2  19511  srgbinom  20253  psgndiflemA  21626  haust1  23385  cnhaus  23387  isreg2  23410  llynlly  23510  restnlly  23515  llyrest  23518  llyidm  23521  nllyidm  23522  cldllycmp  23528  txlly  23669  txnlly  23670  pthaus  23671  txhaus  23680  txkgen  23685  xkohaus  23686  xkococnlem  23692  cmetcaulem  25323  itg2add  25794  ulmdvlem3  26435  nosupprefixmo  27734  noinfprefixmo  27735  nosupno  27737  noinfno  27752  etaslts  27856  cutbdaybnd  27858  cutbdaybnd2  27859  addsproplem6  28037  negsproplem6  28096  mulsproplem13  28191  mulsproplem14  28192  mulsprop  28193  bdayfinbndlem1  28530  ax5seglem6  29074  fusgrfis  29470  wwlksnextfun  30037  umgr2wlkon  30089  connpconn  35533  cvmlift3lem2  35618  cvmlift3lem8  35624  ifscgr  36342  broutsideof3  36424  unblimceq0  36893  paddasslem10  40401  lhpexle2lem  40581  lhpexle3lem  40583  mpaaeu  43675  stoweidlem35  46557  stoweidlem56  46578  stoweidlem59  46581  2arwcat  50169