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

Theorem simprr2 1219
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 1134 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 727 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394  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 206  df-an 395  df-3an 1086
This theorem is referenced by:  poxp2  8154  icodiamlt  15422  psgnunilem2  19457  haust1  23276  cnhaus  23278  isreg2  23301  llynlly  23401  restnlly  23406  llyrest  23409  llyidm  23412  nllyidm  23413  cldllycmp  23419  txlly  23560  txnlly  23561  pthaus  23562  txhaus  23571  txkgen  23576  xkohaus  23577  xkococnlem  23583  cmetcaulem  25236  itg2add  25709  ulmdvlem3  26358  nosupprefixmo  27653  noinfprefixmo  27654  etasslt  27766  scutbdaybnd  27768  scutbdaybnd2  27769  addsproplem6  27911  negsproplem6  27965  mulsproplem13  28048  mulsproplem14  28049  mulsprop  28050  ax5seglem6  28765  n4cyclfrgr  30121  connpconn  34878  cvmlift3lem2  34963  cvmlift3lem8  34969  broutsideof3  35755  unblimceq0  36015  paddasslem10  39334  lhpexle2lem  39514  lhpexle3lem  39516  stoweidlem35  45452  stoweidlem56  45473  stoweidlem59  45476
  Copyright terms: Public domain W3C validator