Theorem simprr3 1221

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

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

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

This theorem is referenced by:  el2xptp0  7851  icodiamlt  15075  psgnunilem2  19018  srgbinom  19696  psgndiflemA  20718  haust1  22411  cnhaus  22413  isreg2  22436  llynlly  22536  restnlly  22541  llyrest  22544  llyidm  22547  nllyidm  22548  cldllycmp  22554  txlly  22695  txnlly  22696  pthaus  22697  txhaus  22706  txkgen  22711  xkohaus  22712  xkococnlem  22718  cmetcaulem  24357  itg2add  24829  ulmdvlem3  25466  ax5seglem6  27205  fusgrfis  27600  wwlksnextfun  28164  umgr2wlkon  28216  connpconn  33097  cvmlift3lem2  33182  cvmlift3lem8  33188  ttrcltr  33702  poxp2  33717  nosupprefixmo  33830  noinfprefixmo  33831  nosupno  33833  noinfno  33848  etasslt  33934  scutbdaybnd  33936  scutbdaybnd2  33937  ifscgr  34273  broutsideof3  34355  unblimceq0  34614  paddasslem10  37770  lhpexle2lem  37950  lhpexle3lem  37952  mpaaeu  40891  stoweidlem35  43466  stoweidlem56  43487  stoweidlem59  43490