Theorem simprr3 1219

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

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

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 209  df-an 399  df-3an 1085

This theorem is referenced by:  el2xptp0  7739  icodiamlt  14798  psgnunilem2  18626  srgbinom  19298  psgndiflemA  20748  haust1  21963  cnhaus  21965  isreg2  21988  llynlly  22088  restnlly  22093  llyrest  22096  llyidm  22099  nllyidm  22100  cldllycmp  22106  txlly  22247  txnlly  22248  pthaus  22249  txhaus  22258  txkgen  22263  xkohaus  22264  xkococnlem  22270  cmetcaulem  23894  itg2add  24363  ulmdvlem3  24993  ax5seglem6  26723  fusgrfis  27115  wwlksnextfun  27679  umgr2wlkon  27732  connpconn  32486  cvmlift3lem2  32571  cvmlift3lem8  32577  noprefixmo  33206  nosupno  33207  scutbdaybnd  33279  ifscgr  33509  broutsideof3  33591  unblimceq0  33850  paddasslem10  36969  lhpexle2lem  37149  lhpexle3lem  37151  mpaaeu  39756  stoweidlem35  42327  stoweidlem56  42348  stoweidlem59  42351