MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  simprr3 Structured version   Visualization version   GIF version

Theorem simprr3 1223
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
StepHypRef Expression
1 simp3 1138 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antll 727 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  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 206  df-an 397  df-3an 1089
This theorem is referenced by:  el2xptp0  7960  poxp2  8067  ttrcltr  9610  icodiamlt  15274  psgnunilem2  19230  srgbinom  19910  psgndiflemA  20952  haust1  22649  cnhaus  22651  isreg2  22674  llynlly  22774  restnlly  22779  llyrest  22782  llyidm  22785  nllyidm  22786  cldllycmp  22792  txlly  22933  txnlly  22934  pthaus  22935  txhaus  22944  txkgen  22949  xkohaus  22950  xkococnlem  22956  cmetcaulem  24598  itg2add  25070  ulmdvlem3  25707  nosupprefixmo  26994  noinfprefixmo  26995  nosupno  26997  noinfno  27012  etasslt  27098  scutbdaybnd  27100  scutbdaybnd2  27101  ax5seglem6  27728  fusgrfis  28123  wwlksnextfun  28688  umgr2wlkon  28740  connpconn  33657  cvmlift3lem2  33742  cvmlift3lem8  33748  addsproplem6  34283  negsproplem6  34320  ifscgr  34561  broutsideof3  34643  unblimceq0  34902  paddasslem10  38224  lhpexle2lem  38404  lhpexle3lem  38406  mpaaeu  41380  stoweidlem35  44171  stoweidlem56  44192  stoweidlem59  44195
  Copyright terms: Public domain W3C validator