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

Theorem simprr2 1216
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simprr2 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)

Proof of Theorem simprr2
StepHypRef Expression
1 simp2 1131 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 725 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1081
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 208  df-an 397  df-3an 1083
This theorem is referenced by:  icodiamlt  14788  psgnunilem2  18545  haust1  21876  cnhaus  21878  isreg2  21901  llynlly  22001  restnlly  22006  llyrest  22009  llyidm  22012  nllyidm  22013  cldllycmp  22019  txlly  22160  txnlly  22161  pthaus  22162  txhaus  22171  txkgen  22176  xkohaus  22177  xkococnlem  22183  cmetcaulem  23806  itg2add  24275  ulmdvlem3  24905  ax5seglem6  26634  n4cyclfrgr  27984  connpconn  32366  cvmlift3lem2  32451  cvmlift3lem8  32457  noprefixmo  33086  scutbdaybnd  33159  broutsideof3  33471  unblimceq0  33730  paddasslem10  36832  lhpexle2lem  37012  lhpexle3lem  37014  stoweidlem35  42182  stoweidlem56  42203  stoweidlem59  42206
  Copyright terms: Public domain W3C validator