Theorem simprr3 1242

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 1156	. 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:  el2xptp0  8030  poxp2  8138  ttrcltr  9695  icodiamlt  15573  psgnunilem2  19671  srgbinom  20419  psgndiflemA  21869  haust1  23632  cnhaus  23634  isreg2  23657  llynlly  23758  restnlly  23763  llyrest  23766  llyidm  23769  nllyidm  23770  cldllycmp  23776  txlly  23917  txnlly  23918  pthaus  23919  txhaus  23928  txkgen  23933  xkohaus  23934  xkococnlem  23940  cmetcaulem  25571  itg2add  26042  ulmdvlem3  26693  nosupprefixmo  27991  noinfprefixmo  27992  nosupno  27994  noinfno  28009  etaslts  28113  cutbdaybnd  28115  cutbdaybnd2  28116  addsproplem6  28294  negsproplem6  28353  mulsproplem13  28448  mulsproplem14  28449  mulsprop  28450  bdayfinbndlem1  28787  ax5seglem6  29446  fusgrfis  29845  wwlksnextfun  30421  umgr2wlkon  30473  connpconn  35921  cvmlift3lem2  36006  cvmlift3lem8  36012  ifscgr  36731  broutsideof3  36813  unblimceq0  37295  paddasslem10  40806  lhpexle2lem  40986  lhpexle3lem  40988  mpaaeu  44095  stoweidlem35  46967  stoweidlem56  46988  stoweidlem59  46991  2arwcat  50630