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

Theorem simprr1 1272
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 1130 . 2 ((𝜑𝜓𝜒) → 𝜑)
21ad2antll 700 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  sqrmo  14199  icodiamlt  14381  psgnunilem2  18121  haust1  21376  cnhaus  21378  isreg2  21401  llynlly  21500  restnlly  21505  llyrest  21508  llyidm  21511  nllyidm  21512  cldllycmp  21518  txlly  21659  txnlly  21660  pthaus  21661  txhaus  21670  txkgen  21675  xkohaus  21676  xkococnlem  21682  hauspwpwf1  22010  itg2add  23745  ulmdvlem3  24375  ax5seglem6  26034  fusgrfis  26444  umgr2wlkon  27096  numclwwlk5  27584  connpconn  31552  cvmliftmolem2  31599  cvmlift2lem10  31629  cvmlift3lem2  31637  cvmlift3lem8  31643  nosupno  32183  scutbdaybnd  32255  broutsideof3  32567  unblimceq0  32832  paddasslem10  35633  lhpexle2lem  35813  lhpexle3lem  35815  cdlemj3  36628  cdlemkid4  36739  mpaaeu  38242  stoweidlem35  40765  stoweidlem56  40786  stoweidlem59  40789
  Copyright terms: Public domain W3C validator