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

Theorem simprr2 1275
 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 1132 . 2 ((𝜑𝜓𝜒) → 𝜓)
21ad2antll 767 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1072 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 197  df-an 385  df-3an 1074 This theorem is referenced by:  icodiamlt  14393  psgnunilem2  18135  haust1  21378  cnhaus  21380  isreg2  21403  llynlly  21502  restnlly  21507  llyrest  21510  llyidm  21513  nllyidm  21514  cldllycmp  21520  txlly  21661  txnlly  21662  pthaus  21663  txhaus  21672  txkgen  21677  xkohaus  21678  xkococnlem  21684  cmetcaulem  23306  itg2add  23745  ulmdvlem3  24375  ax5seglem6  26034  n4cyclfrgr  27466  connpconn  31545  cvmlift3lem2  31630  cvmlift3lem8  31636  noprefixmo  32175  scutbdaybnd  32248  broutsideof3  32560  unblimceq0  32825  paddasslem10  35636  lhpexle2lem  35816  lhpexle3lem  35818  stoweidlem35  40773  stoweidlem56  40794  stoweidlem59  40797
 Copyright terms: Public domain W3C validator