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

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

Proof of Theorem simprr1
StepHypRef Expression
1 simp1 1129 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antll 725 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1080
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 1082
This theorem is referenced by:  sqrmo  14449  icodiamlt  14633  psgnunilem2  18358  haust1  21648  cnhaus  21650  isreg2  21673  llynlly  21773  restnlly  21778  llyrest  21781  llyidm  21784  nllyidm  21785  cldllycmp  21791  txlly  21932  txnlly  21933  pthaus  21934  txhaus  21943  txkgen  21948  xkohaus  21949  xkococnlem  21955  hauspwpwf1  22283  itg2add  24047  ulmdvlem3  24677  ax5seglem6  26407  fusgrfis  26799  umgr2wlkon  27415  numclwwlk5  27855  connpconn  32092  cvmliftmolem2  32139  cvmlift2lem10  32169  cvmlift3lem2  32177  cvmlift3lem8  32183  nosupno  32814  scutbdaybnd  32886  broutsideof3  33198  unblimceq0  33457  paddasslem10  36517  lhpexle2lem  36697  lhpexle3lem  36699  cdlemj3  37511  cdlemkid4  37622  mpaaeu  39256  stoweidlem35  41884  stoweidlem56  41905  stoweidlem59  41908
  Copyright terms: Public domain W3C validator