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  8017  poxp2  8124  ttrcltr  9675  icodiamlt  15410  psgnunilem2  19431  srgbinom  20146  psgndiflemA  21516  haust1  23245  cnhaus  23247  isreg2  23270  llynlly  23370  restnlly  23375  llyrest  23378  llyidm  23381  nllyidm  23382  cldllycmp  23388  txlly  23529  txnlly  23530  pthaus  23531  txhaus  23540  txkgen  23545  xkohaus  23546  xkococnlem  23552  cmetcaulem  25194  itg2add  25666  ulmdvlem3  26317  nosupprefixmo  27618  noinfprefixmo  27619  nosupno  27621  noinfno  27636  etasslt  27731  scutbdaybnd  27733  scutbdaybnd2  27734  addsproplem6  27887  negsproplem6  27945  mulsproplem13  28037  mulsproplem14  28038  mulsprop  28039  ax5seglem6  28867  fusgrfis  29263  wwlksnextfun  29834  umgr2wlkon  29886  connpconn  35222  cvmlift3lem2  35307  cvmlift3lem8  35313  ifscgr  36027  broutsideof3  36109  unblimceq0  36490  paddasslem10  39818  lhpexle2lem  39998  lhpexle3lem  40000  mpaaeu  43132  stoweidlem35  46026  stoweidlem56  46047  stoweidlem59  46050  2arwcat  49579