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

Theorem simprr3 1220
 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 1135 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antll 728 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∧ w3a 1084 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 210  df-an 400  df-3an 1086 This theorem is referenced by:  el2xptp0  7722  icodiamlt  14791  psgnunilem2  18619  srgbinom  19292  psgndiflemA  20294  haust1  21961  cnhaus  21963  isreg2  21986  llynlly  22086  restnlly  22091  llyrest  22094  llyidm  22097  nllyidm  22098  cldllycmp  22104  txlly  22245  txnlly  22246  pthaus  22247  txhaus  22256  txkgen  22261  xkohaus  22262  xkococnlem  22268  cmetcaulem  23896  itg2add  24367  ulmdvlem3  25001  ax5seglem6  26732  fusgrfis  27124  wwlksnextfun  27688  umgr2wlkon  27740  connpconn  32596  cvmlift3lem2  32681  cvmlift3lem8  32687  noprefixmo  33316  nosupno  33317  scutbdaybnd  33389  ifscgr  33619  broutsideof3  33701  unblimceq0  33960  paddasslem10  37124  lhpexle2lem  37304  lhpexle3lem  37306  mpaaeu  40091  stoweidlem35  42674  stoweidlem56  42695  stoweidlem59  42698
 Copyright terms: Public domain W3C validator