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  8036  poxp2  8144  ttrcltr  9698  icodiamlt  15527  psgnunilem2  19626  srgbinom  20374  psgndiflemA  21818  haust1  23581  cnhaus  23583  isreg2  23606  llynlly  23707  restnlly  23712  llyrest  23715  llyidm  23718  nllyidm  23719  cldllycmp  23725  txlly  23866  txnlly  23867  pthaus  23868  txhaus  23877  txkgen  23882  xkohaus  23883  xkococnlem  23889  cmetcaulem  25520  itg2add  25991  ulmdvlem3  26638  nosupprefixmo  27937  noinfprefixmo  27938  nosupno  27940  noinfno  27955  etaslts  28059  cutbdaybnd  28061  cutbdaybnd2  28062  addsproplem6  28240  negsproplem6  28299  mulsproplem13  28394  mulsproplem14  28395  mulsprop  28396  bdayfinbndlem1  28733  ax5seglem6  29392  fusgrfis  29791  wwlksnextfun  30367  umgr2wlkon  30419  connpconn  35816  cvmlift3lem2  35901  cvmlift3lem8  35907  ifscgr  36626  broutsideof3  36708  unblimceq0  37206  paddasslem10  40704  lhpexle2lem  40884  lhpexle3lem  40886  mpaaeu  43993  stoweidlem35  46865  stoweidlem56  46886  stoweidlem59  46889  2arwcat  50528