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  7963  poxp2  8068  ttrcltr  9601  icodiamlt  15337  psgnunilem2  19400  srgbinom  20142  psgndiflemA  21531  haust1  23260  cnhaus  23262  isreg2  23285  llynlly  23385  restnlly  23390  llyrest  23393  llyidm  23396  nllyidm  23397  cldllycmp  23403  txlly  23544  txnlly  23545  pthaus  23546  txhaus  23555  txkgen  23560  xkohaus  23561  xkococnlem  23567  cmetcaulem  25208  itg2add  25680  ulmdvlem3  26331  nosupprefixmo  27632  noinfprefixmo  27633  nosupno  27635  noinfno  27650  etasslt  27747  scutbdaybnd  27749  scutbdaybnd2  27750  addsproplem6  27910  negsproplem6  27968  mulsproplem13  28060  mulsproplem14  28061  mulsprop  28062  ax5seglem6  28905  fusgrfis  29301  wwlksnextfun  29869  umgr2wlkon  29921  connpconn  35247  cvmlift3lem2  35332  cvmlift3lem8  35338  ifscgr  36057  broutsideof3  36139  unblimceq0  36520  paddasslem10  39847  lhpexle2lem  40027  lhpexle3lem  40029  mpaaeu  43162  stoweidlem35  46052  stoweidlem56  46073  stoweidlem59  46076  2arwcat  49611