Theorem simprr3 1240

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  el2xptp0  8021  poxp2  8127  ttrcltr  9673  icodiamlt  15479  psgnunilem2  19556  srgbinom  20304  psgndiflemA  21711  haust1  23470  cnhaus  23472  isreg2  23495  llynlly  23595  restnlly  23600  llyrest  23603  llyidm  23606  nllyidm  23607  cldllycmp  23613  txlly  23754  txnlly  23755  pthaus  23756  txhaus  23765  txkgen  23770  xkohaus  23771  xkococnlem  23777  cmetcaulem  25408  itg2add  25879  ulmdvlem3  26523  nosupprefixmo  27822  noinfprefixmo  27823  nosupno  27825  noinfno  27840  etaslts  27944  cutbdaybnd  27946  cutbdaybnd2  27947  addsproplem6  28125  negsproplem6  28184  mulsproplem13  28279  mulsproplem14  28280  mulsprop  28281  bdayfinbndlem1  28618  ax5seglem6  29193  fusgrfis  29589  wwlksnextfun  30156  umgr2wlkon  30208  connpconn  35598  cvmlift3lem2  35683  cvmlift3lem8  35689  ifscgr  36407  broutsideof3  36489  unblimceq0  36958  paddasslem10  40465  lhpexle2lem  40645  lhpexle3lem  40647  mpaaeu  43739  stoweidlem35  46607  stoweidlem56  46628  stoweidlem59  46631  2arwcat  50229