Theorem simprr3 1242

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

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 402  df-3an 1105

This theorem is used by:  el2xptp0  8071  poxp2  8187  ttrcltr  9744  icodiamlt  15634  psgnunilem2  19739  srgbinom  20487  psgndiflemA  21937  haust1  23700  cnhaus  23702  isreg2  23725  llynlly  23826  restnlly  23831  llyrest  23834  llyidm  23837  nllyidm  23838  cldllycmp  23844  txlly  23985  txnlly  23986  pthaus  23987  txhaus  23996  txkgen  24001  xkohaus  24002  xkococnlem  24008  cmetcaulem  25639  itg2add  26110  ulmdvlem3  26759  nosupprefixmo  28087  noinfprefixmo  28088  nosupno  28090  noinfno  28105  etaslts  28209  cutbdaybnd  28211  cutbdaybnd2  28212  addsproplem6  28390  negsproplem6  28449  mulsproplem13  28544  mulsproplem14  28545  mulsprop  28546  bdayfinbndlem1  28883  ax5seglem6  29542  fusgrfis  29941  wwlksnextfun  30517  umgr2wlkon  30569  connpconn  36167  cvmlift3lem2  36252  cvmlift3lem8  36258  ifscgr  36987  broutsideof3  37069  unblimceq0  37551  paddasslem10  41078  lhpexle2lem  41258  lhpexle3lem  41260  mpaaeu  44344  stoweidlem35  47250  stoweidlem56  47271  stoweidlem59  47274  2arwcat  50943