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

Theorem simprr3 1131
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.)
Assertion
Ref Expression
simprr3 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)

Proof of Theorem simprr3
StepHypRef Expression
1 simpr3 1089 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜒)
21adantl 481 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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 1056
This theorem is referenced by:  el2xptp0  7256  icodiamlt  14218  psgnunilem2  17961  srgbinom  18591  psgndiflemA  19995  haust1  21204  cnhaus  21206  isreg2  21229  llynlly  21328  restnlly  21333  llyrest  21336  llyidm  21339  nllyidm  21340  cldllycmp  21346  txlly  21487  txnlly  21488  pthaus  21489  txhaus  21498  txkgen  21503  xkohaus  21504  xkococnlem  21510  cmetcaulem  23132  itg2add  23571  ulmdvlem3  24201  ax5seglem6  25859  fusgrfis  26267  wwlksnextfun  26861  umgr2wlkon  26915  connpconn  31343  cvmlift3lem2  31428  cvmlift3lem8  31434  noprefixmo  31973  nosupno  31974  scutbdaybnd  32046  ifscgr  32276  broutsideof3  32358  unblimceq0  32623  paddasslem10  35433  lhpexle2lem  35613  lhpexle3lem  35615  mpaaeu  38037  stoweidlem35  40570  stoweidlem56  40591  stoweidlem59  40594
  Copyright terms: Public domain W3C validator