Theorem simprr3 1225

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 1139	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜒)
2	1	ad2antll 730	1 ⊢ ((𝜏 ∧ (𝜃 ∧ (𝜑 ∧ 𝜓 ∧ 𝜒))) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 1089

This theorem is referenced by:  el2xptp0  7990  poxp2  8095  ttrcltr  9637  icodiamlt  15373  psgnunilem2  19436  srgbinom  20178  psgndiflemA  21568  haust1  23308  cnhaus  23310  isreg2  23333  llynlly  23433  restnlly  23438  llyrest  23441  llyidm  23444  nllyidm  23445  cldllycmp  23451  txlly  23592  txnlly  23593  pthaus  23594  txhaus  23603  txkgen  23608  xkohaus  23609  xkococnlem  23615  cmetcaulem  25256  itg2add  25728  ulmdvlem3  26379  nosupprefixmo  27680  noinfprefixmo  27681  nosupno  27683  noinfno  27698  etaslts  27801  cutbdaybnd  27803  cutbdaybnd2  27804  addsproplem6  27982  negsproplem6  28041  mulsproplem13  28136  mulsproplem14  28137  mulsprop  28138  bdayfinbndlem1  28475  ax5seglem6  29019  fusgrfis  29415  wwlksnextfun  29983  umgr2wlkon  30035  connpconn  35448  cvmlift3lem2  35533  cvmlift3lem8  35539  ifscgr  36257  broutsideof3  36339  unblimceq0  36726  paddasslem10  40194  lhpexle2lem  40374  lhpexle3lem  40376  mpaaeu  43496  stoweidlem35  46382  stoweidlem56  46403  stoweidlem59  46406  2arwcat  49948