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  8047  poxp2  8160  ttrcltr  9718  icodiamlt  15606  psgnunilem2  19710  srgbinom  20458  psgndiflemA  21908  haust1  23671  cnhaus  23673  isreg2  23696  llynlly  23797  restnlly  23802  llyrest  23805  llyidm  23808  nllyidm  23809  cldllycmp  23815  txlly  23956  txnlly  23957  pthaus  23958  txhaus  23967  txkgen  23972  xkohaus  23973  xkococnlem  23979  cmetcaulem  25610  itg2add  26081  ulmdvlem3  26730  nosupprefixmo  28058  noinfprefixmo  28059  nosupno  28061  noinfno  28076  etaslts  28180  cutbdaybnd  28182  cutbdaybnd2  28183  addsproplem6  28361  negsproplem6  28420  mulsproplem13  28515  mulsproplem14  28516  mulsprop  28517  bdayfinbndlem1  28854  ax5seglem6  29513  fusgrfis  29912  wwlksnextfun  30488  umgr2wlkon  30540  connpconn  36069  cvmlift3lem2  36154  cvmlift3lem8  36160  ifscgr  36884  broutsideof3  36966  unblimceq0  37448  paddasslem10  40962  lhpexle2lem  41142  lhpexle3lem  41144  mpaaeu  44228  stoweidlem35  47121  stoweidlem56  47142  stoweidlem59  47145  2arwcat  50784