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  7980  poxp2  8084  ttrcltr  9626  icodiamlt  15389  psgnunilem2  19459  srgbinom  20201  psgndiflemA  21589  haust1  23326  cnhaus  23328  isreg2  23351  llynlly  23451  restnlly  23456  llyrest  23459  llyidm  23462  nllyidm  23463  cldllycmp  23469  txlly  23610  txnlly  23611  pthaus  23612  txhaus  23621  txkgen  23626  xkohaus  23627  xkococnlem  23633  cmetcaulem  25264  itg2add  25735  ulmdvlem3  26382  nosupprefixmo  27683  noinfprefixmo  27684  nosupno  27686  noinfno  27701  etaslts  27804  cutbdaybnd  27806  cutbdaybnd2  27807  addsproplem6  27985  negsproplem6  28044  mulsproplem13  28139  mulsproplem14  28140  mulsprop  28141  bdayfinbndlem1  28478  ax5seglem6  29022  fusgrfis  29418  wwlksnextfun  29986  umgr2wlkon  30038  connpconn  35438  cvmlift3lem2  35523  cvmlift3lem8  35529  ifscgr  36247  broutsideof3  36329  unblimceq0  36780  paddasslem10  40286  lhpexle2lem  40466  lhpexle3lem  40468  mpaaeu  43593  stoweidlem35  46478  stoweidlem56  46499  stoweidlem59  46502  2arwcat  50072