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

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

Proof of Theorem simprr1
StepHypRef Expression
1 simpr1 1060 . 2 ((𝜃 ∧ (𝜑𝜓𝜒)) → 𝜑)
21adantl 481 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜑)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031 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 196  df-an 385  df-3an 1033 This theorem is referenced by:  sqrmo  13840  icodiamlt  14022  psgnunilem2  17738  haust1  20966  cnhaus  20968  isreg2  20991  llynlly  21090  restnlly  21095  llyrest  21098  llyidm  21101  nllyidm  21102  cldllycmp  21108  txlly  21249  txnlly  21250  pthaus  21251  txhaus  21260  txkgen  21265  xkohaus  21266  xkococnlem  21272  hauspwpwf1  21601  itg2add  23332  ulmdvlem3  23960  ax5seglem6  25614  frg2woteqm  26586  numclwlk1lem2f  26619  numclwwlk5  26639  conpcon  30471  cvmliftmolem2  30518  cvmlift2lem10  30548  cvmlift3lem2  30556  cvmlift3lem8  30562  broutsideof3  31403  unblimceq0  31668  paddasslem10  34133  lhpexle2lem  34313  lhpexle3lem  34315  cdlemj3  35129  cdlemkid4  35240  mpaaeu  36739  stoweidlem35  38928  stoweidlem56  38949  stoweidlem59  38952  fusgrfis  40549  umgr2wlkon  41157  av-numclwlk1lem2f  41522  av-numclwwlk5  41542
 Copyright terms: Public domain W3C validator