Theorem simprr3 1225

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1087

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 207  df-an 396  df-3an 1089

This theorem is referenced by:  el2xptp0  7982  poxp2  8087  ttrcltr  9629  icodiamlt  15365  psgnunilem2  19428  srgbinom  20170  psgndiflemA  21560  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  25248  itg2add  25720  ulmdvlem3  26371  nosupprefixmo  27672  noinfprefixmo  27673  nosupno  27675  noinfno  27690  etasslt  27791  scutbdaybnd  27793  scutbdaybnd2  27794  addsproplem6  27956  negsproplem6  28015  mulsproplem13  28110  mulsproplem14  28111  mulsprop  28112  bdayfinbndlem1  28446  ax5seglem6  28990  fusgrfis  29386  wwlksnextfun  29954  umgr2wlkon  30006  connpconn  35410  cvmlift3lem2  35495  cvmlift3lem8  35501  ifscgr  36219  broutsideof3  36301  unblimceq0  36682  paddasslem10  40126  lhpexle2lem  40306  lhpexle3lem  40308  mpaaeu  43428  stoweidlem35  46315  stoweidlem56  46336  stoweidlem59  46339  2arwcat  49881