Theorem simprr3 1220

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

Syntax hints:   → wi 4   ∧ wa 394   ∧ w3a 1084

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 206  df-an 395  df-3an 1086

This theorem is referenced by:  el2xptp0  8039  poxp2  8146  ttrcltr  9739  icodiamlt  15414  psgnunilem2  19454  srgbinom  20175  psgndiflemA  21537  haust1  23286  cnhaus  23288  isreg2  23311  llynlly  23411  restnlly  23416  llyrest  23419  llyidm  23422  nllyidm  23423  cldllycmp  23429  txlly  23570  txnlly  23571  pthaus  23572  txhaus  23581  txkgen  23586  xkohaus  23587  xkococnlem  23593  cmetcaulem  25246  itg2add  25719  ulmdvlem3  26368  nosupprefixmo  27663  noinfprefixmo  27664  nosupno  27666  noinfno  27681  etasslt  27776  scutbdaybnd  27778  scutbdaybnd2  27779  addsproplem6  27921  negsproplem6  27975  mulsproplem13  28062  mulsproplem14  28063  mulsprop  28064  ax5seglem6  28801  fusgrfis  29199  wwlksnextfun  29765  umgr2wlkon  29817  connpconn  34915  cvmlift3lem2  35000  cvmlift3lem8  35006  ifscgr  35710  broutsideof3  35792  unblimceq0  36052  paddasslem10  39371  lhpexle2lem  39551  lhpexle3lem  39553  mpaaeu  42639  stoweidlem35  45486  stoweidlem56  45507  stoweidlem59  45510