Theorem simprr3 1224

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

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

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 1088

This theorem is referenced by:  el2xptp0  7977  poxp2  8082  ttrcltr  9616  icodiamlt  15355  psgnunilem2  19417  srgbinom  20159  psgndiflemA  21548  haust1  23277  cnhaus  23279  isreg2  23302  llynlly  23402  restnlly  23407  llyrest  23410  llyidm  23413  nllyidm  23414  cldllycmp  23420  txlly  23561  txnlly  23562  pthaus  23563  txhaus  23572  txkgen  23577  xkohaus  23578  xkococnlem  23584  cmetcaulem  25225  itg2add  25697  ulmdvlem3  26348  nosupprefixmo  27649  noinfprefixmo  27650  nosupno  27652  noinfno  27667  etasslt  27764  scutbdaybnd  27766  scutbdaybnd2  27767  addsproplem6  27927  negsproplem6  27985  mulsproplem13  28077  mulsproplem14  28078  mulsprop  28079  ax5seglem6  28923  fusgrfis  29319  wwlksnextfun  29887  umgr2wlkon  29939  connpconn  35290  cvmlift3lem2  35375  cvmlift3lem8  35381  ifscgr  36099  broutsideof3  36181  unblimceq0  36562  paddasslem10  39938  lhpexle2lem  40118  lhpexle3lem  40120  mpaaeu  43257  stoweidlem35  46147  stoweidlem56  46168  stoweidlem59  46171  2arwcat  49715