Theorem simprr3 1222

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 1137	. 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  8060  poxp2  8167  ttrcltr  9754  icodiamlt  15471  psgnunilem2  19528  srgbinom  20249  psgndiflemA  21637  haust1  23376  cnhaus  23378  isreg2  23401  llynlly  23501  restnlly  23506  llyrest  23509  llyidm  23512  nllyidm  23513  cldllycmp  23519  txlly  23660  txnlly  23661  pthaus  23662  txhaus  23671  txkgen  23676  xkohaus  23677  xkococnlem  23683  cmetcaulem  25336  itg2add  25809  ulmdvlem3  26460  nosupprefixmo  27760  noinfprefixmo  27761  nosupno  27763  noinfno  27778  etasslt  27873  scutbdaybnd  27875  scutbdaybnd2  27876  addsproplem6  28022  negsproplem6  28080  mulsproplem13  28169  mulsproplem14  28170  mulsprop  28171  ax5seglem6  28964  fusgrfis  29362  wwlksnextfun  29928  umgr2wlkon  29980  connpconn  35220  cvmlift3lem2  35305  cvmlift3lem8  35311  ifscgr  36026  broutsideof3  36108  unblimceq0  36490  paddasslem10  39812  lhpexle2lem  39992  lhpexle3lem  39994  mpaaeu  43139  stoweidlem35  45991  stoweidlem56  46012  stoweidlem59  46015