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

Theorem simprr2 1290
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 1168 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 721 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 385  w3a 1108
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 199  df-an 386  df-3an 1110
This theorem is referenced by:  icodiamlt  14515  psgnunilem2  18228  haust1  21485  cnhaus  21487  isreg2  21510  llynlly  21609  restnlly  21614  llyrest  21617  llyidm  21620  nllyidm  21621  cldllycmp  21627  txlly  21768  txnlly  21769  pthaus  21770  txhaus  21779  txkgen  21784  xkohaus  21785  xkococnlem  21791  cmetcaulem  23414  itg2add  23867  ulmdvlem3  24497  ax5seglem6  26171  n4cyclfrgr  27640  connpconn  31734  cvmlift3lem2  31819  cvmlift3lem8  31825  noprefixmo  32361  scutbdaybnd  32434  broutsideof3  32746  unblimceq0  33006  paddasslem10  35850  lhpexle2lem  36030  lhpexle3lem  36032  stoweidlem35  40995  stoweidlem56  41016  stoweidlem59  41019
  Copyright terms: Public domain W3C validator