Theorem simprr3 1224

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

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

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 1088

This theorem is referenced by:  el2xptp0  7978  poxp2  8083  ttrcltr  9631  icodiamlt  15363  psgnunilem2  19392  srgbinom  20134  psgndiflemA  21526  haust1  23255  cnhaus  23257  isreg2  23280  llynlly  23380  restnlly  23385  llyrest  23388  llyidm  23391  nllyidm  23392  cldllycmp  23398  txlly  23539  txnlly  23540  pthaus  23541  txhaus  23550  txkgen  23555  xkohaus  23556  xkococnlem  23562  cmetcaulem  25204  itg2add  25676  ulmdvlem3  26327  nosupprefixmo  27628  noinfprefixmo  27629  nosupno  27631  noinfno  27646  etasslt  27742  scutbdaybnd  27744  scutbdaybnd2  27745  addsproplem6  27904  negsproplem6  27962  mulsproplem13  28054  mulsproplem14  28055  mulsprop  28056  ax5seglem6  28897  fusgrfis  29293  wwlksnextfun  29861  umgr2wlkon  29913  connpconn  35207  cvmlift3lem2  35292  cvmlift3lem8  35298  ifscgr  36017  broutsideof3  36099  unblimceq0  36480  paddasslem10  39808  lhpexle2lem  39988  lhpexle3lem  39990  mpaaeu  43123  stoweidlem35  46017  stoweidlem56  46038  stoweidlem59  46041  2arwcat  49573