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

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

Proof of Theorem simprr2
StepHypRef Expression
1 simpr2 1066 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜓)
21adantl 482 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  icodiamlt  14108  psgnunilem2  17836  haust1  21066  cnhaus  21068  isreg2  21091  llynlly  21190  restnlly  21195  llyrest  21198  llyidm  21201  nllyidm  21202  cldllycmp  21208  txlly  21349  txnlly  21350  pthaus  21351  txhaus  21360  txkgen  21365  xkohaus  21366  xkococnlem  21372  cmetcaulem  22994  itg2add  23432  ulmdvlem3  24060  ax5seglem6  25714  n4cyclfrgr  27019  numclwlk1lem2f  27080  connpconn  30922  cvmlift3lem2  31007  cvmlift3lem8  31013  broutsideof3  31872  unblimceq0  32137  paddasslem10  34592  lhpexle2lem  34772  lhpexle3lem  34774  stoweidlem35  39556  stoweidlem56  39577  stoweidlem59  39580
  Copyright terms: Public domain W3C validator