Theorem simprr3 1221

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

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

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 206  df-an 396  df-3an 1087

This theorem is referenced by:  el2xptp0  8034  poxp2  8142  ttrcltr  9731  icodiamlt  15406  psgnunilem2  19441  srgbinom  20162  psgndiflemA  21520  haust1  23243  cnhaus  23245  isreg2  23268  llynlly  23368  restnlly  23373  llyrest  23376  llyidm  23379  nllyidm  23380  cldllycmp  23386  txlly  23527  txnlly  23528  pthaus  23529  txhaus  23538  txkgen  23543  xkohaus  23544  xkococnlem  23550  cmetcaulem  25203  itg2add  25676  ulmdvlem3  26325  nosupprefixmo  27620  noinfprefixmo  27621  nosupno  27623  noinfno  27638  etasslt  27733  scutbdaybnd  27735  scutbdaybnd2  27736  addsproplem6  27878  negsproplem6  27932  mulsproplem13  28015  mulsproplem14  28016  mulsprop  28017  ax5seglem6  28732  fusgrfis  29130  wwlksnextfun  29696  umgr2wlkon  29748  connpconn  34781  cvmlift3lem2  34866  cvmlift3lem8  34872  ifscgr  35576  broutsideof3  35658  unblimceq0  35918  paddasslem10  39239  lhpexle2lem  39419  lhpexle3lem  39421  mpaaeu  42496  stoweidlem35  45346  stoweidlem56  45367  stoweidlem59  45370