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

Theorem simprr1 1222
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 1137 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antll 728 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  w3a 1088
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 398  df-3an 1090
This theorem is referenced by:  poxp2  8080  sqrmo  15143  icodiamlt  15327  psgnunilem2  19284  haust1  22719  cnhaus  22721  isreg2  22744  llynlly  22844  restnlly  22849  llyrest  22852  llyidm  22855  nllyidm  22856  cldllycmp  22862  txlly  23003  txnlly  23004  pthaus  23005  txhaus  23014  txkgen  23019  xkohaus  23020  xkococnlem  23026  hauspwpwf1  23354  itg2add  25140  ulmdvlem3  25777  nosupno  27067  noinfno  27082  etasslt  27174  scutbdaybnd  27176  scutbdaybnd2  27177  addsproplem6  27308  negsproplem6  27353  ax5seglem6  27925  fusgrfis  28320  umgr2wlkon  28937  numclwwlk5  29374  connpconn  33869  cvmliftmolem2  33916  cvmlift2lem10  33946  cvmlift3lem2  33954  cvmlift3lem8  33960  broutsideof3  34740  unblimceq0  34999  paddasslem10  38321  lhpexle2lem  38501  lhpexle3lem  38503  cdlemj3  39315  cdlemkid4  39426  mpaaeu  41506  stoweidlem35  44350  stoweidlem56  44371  stoweidlem59  44374
  Copyright terms: Public domain W3C validator