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 726 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  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 396  df-3an 1086
This theorem is referenced by:  poxp2  8126  icodiamlt  15385  psgnunilem2  19412  haust1  23206  cnhaus  23208  isreg2  23231  llynlly  23331  restnlly  23336  llyrest  23339  llyidm  23342  nllyidm  23343  cldllycmp  23349  txlly  23490  txnlly  23491  pthaus  23492  txhaus  23501  txkgen  23506  xkohaus  23507  xkococnlem  23513  cmetcaulem  25166  itg2add  25639  ulmdvlem3  26288  nosupprefixmo  27583  noinfprefixmo  27584  etasslt  27696  scutbdaybnd  27698  scutbdaybnd2  27699  addsproplem6  27841  negsproplem6  27895  mulsproplem13  27978  mulsproplem14  27979  mulsprop  27980  ax5seglem6  28695  n4cyclfrgr  30048  connpconn  34753  cvmlift3lem2  34838  cvmlift3lem8  34844  broutsideof3  35630  unblimceq0  35890  paddasslem10  39212  lhpexle2lem  39392  lhpexle3lem  39394  stoweidlem35  45305  stoweidlem56  45326  stoweidlem59  45329
  Copyright terms: Public domain W3C validator