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

Theorem simprr1 1221
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 1136 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antll 727 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087
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 397  df-3an 1089
This theorem is referenced by:  poxp2  8074  sqrmo  15135  icodiamlt  15319  psgnunilem2  19275  haust1  22701  cnhaus  22703  isreg2  22726  llynlly  22826  restnlly  22831  llyrest  22834  llyidm  22837  nllyidm  22838  cldllycmp  22844  txlly  22985  txnlly  22986  pthaus  22987  txhaus  22996  txkgen  23001  xkohaus  23002  xkococnlem  23008  hauspwpwf1  23336  itg2add  25122  ulmdvlem3  25759  nosupno  27049  noinfno  27064  etasslt  27150  scutbdaybnd  27152  scutbdaybnd2  27153  addsproplem6  27284  negsproplem6  27329  ax5seglem6  27881  fusgrfis  28276  umgr2wlkon  28893  numclwwlk5  29330  connpconn  33820  cvmliftmolem2  33867  cvmlift2lem10  33897  cvmlift3lem2  33905  cvmlift3lem8  33911  broutsideof3  34702  unblimceq0  34961  paddasslem10  38283  lhpexle2lem  38463  lhpexle3lem  38465  cdlemj3  39277  cdlemkid4  39388  mpaaeu  41455  stoweidlem35  44248  stoweidlem56  44269  stoweidlem59  44272
  Copyright terms: Public domain W3C validator