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  8041  poxp2  8148  ttrcltr  9741  icodiamlt  15418  psgnunilem2  19462  srgbinom  20183  psgndiflemA  21550  haust1  23300  cnhaus  23302  isreg2  23325  llynlly  23425  restnlly  23430  llyrest  23433  llyidm  23436  nllyidm  23437  cldllycmp  23443  txlly  23584  txnlly  23585  pthaus  23586  txhaus  23595  txkgen  23600  xkohaus  23601  xkococnlem  23607  cmetcaulem  25260  itg2add  25733  ulmdvlem3  26383  nosupprefixmo  27679  noinfprefixmo  27680  nosupno  27682  noinfno  27697  etasslt  27792  scutbdaybnd  27794  scutbdaybnd2  27795  addsproplem6  27937  negsproplem6  27991  mulsproplem13  28078  mulsproplem14  28079  mulsprop  28080  ax5seglem6  28817  fusgrfis  29215  wwlksnextfun  29781  umgr2wlkon  29833  connpconn  34976  cvmlift3lem2  35061  cvmlift3lem8  35067  ifscgr  35771  broutsideof3  35853  unblimceq0  36113  paddasslem10  39432  lhpexle2lem  39612  lhpexle3lem  39614  mpaaeu  42716  stoweidlem35  45561  stoweidlem56  45582  stoweidlem59  45585