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

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

Proof of Theorem simprr3
StepHypRef Expression
1 simpr3 1067 . 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:  el2xptp0  7160  icodiamlt  14103  psgnunilem2  17831  srgbinom  18461  psgndiflemA  19861  haust1  21061  cnhaus  21063  isreg2  21086  llynlly  21185  restnlly  21190  llyrest  21193  llyidm  21196  nllyidm  21197  cldllycmp  21203  txlly  21344  txnlly  21345  pthaus  21346  txhaus  21355  txkgen  21360  xkohaus  21361  xkococnlem  21367  cmetcaulem  22989  itg2add  23427  ulmdvlem3  24055  ax5seglem6  25709  fusgrfis  26104  wwlksnextfun  26656  umgr2wlkon  26709  connpconn  30917  cvmlift3lem2  31002  cvmlift3lem8  31008  nosino  31567  ifscgr  31785  broutsideof3  31867  unblimceq0  32132  paddasslem10  34581  lhpexle2lem  34761  lhpexle3lem  34763  mpaaeu  37187  stoweidlem35  39546  stoweidlem56  39567  stoweidlem59  39570
  Copyright terms: Public domain W3C validator