Theorem simprr3 1241

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 400   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  el2xptp0  8031  poxp2  8137  ttrcltr  9683  icodiamlt  15496  psgnunilem2  19571  srgbinom  20319  psgndiflemA  21762  haust1  23520  cnhaus  23522  isreg2  23545  llynlly  23645  restnlly  23650  llyrest  23653  llyidm  23656  nllyidm  23657  cldllycmp  23663  txlly  23804  txnlly  23805  pthaus  23806  txhaus  23815  txkgen  23820  xkohaus  23821  xkococnlem  23827  cmetcaulem  25458  itg2add  25929  ulmdvlem3  26576  nosupprefixmo  27875  noinfprefixmo  27876  nosupno  27878  noinfno  27893  etaslts  27997  cutbdaybnd  27999  cutbdaybnd2  28000  addsproplem6  28178  negsproplem6  28237  mulsproplem13  28332  mulsproplem14  28333  mulsprop  28334  bdayfinbndlem1  28671  ax5seglem6  29295  fusgrfis  29691  wwlksnextfun  30258  umgr2wlkon  30310  connpconn  35735  cvmlift3lem2  35820  cvmlift3lem8  35826  ifscgr  36544  broutsideof3  36626  unblimceq0  37124  paddasslem10  40631  lhpexle2lem  40811  lhpexle3lem  40813  mpaaeu  43905  stoweidlem35  46777  stoweidlem56  46798  stoweidlem59  46801  2arwcat  50406