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

Theorem simprr3 1223
Description: Simplification of conjunction. (Contributed by NM, 9-Mar-2012.) (Proof shortened by Wolf Lammen, 23-Jun-2022.)
Assertion
Ref Expression
simprr3 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)

Proof of Theorem simprr3
StepHypRef Expression
1 simp3 1138 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antll 729 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086
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 207  df-an 396  df-3an 1088
This theorem is referenced by:  el2xptp0  8062  poxp2  8169  ttrcltr  9757  icodiamlt  15475  psgnunilem2  19514  srgbinom  20229  psgndiflemA  21620  haust1  23361  cnhaus  23363  isreg2  23386  llynlly  23486  restnlly  23491  llyrest  23494  llyidm  23497  nllyidm  23498  cldllycmp  23504  txlly  23645  txnlly  23646  pthaus  23647  txhaus  23656  txkgen  23661  xkohaus  23662  xkococnlem  23668  cmetcaulem  25323  itg2add  25795  ulmdvlem3  26446  nosupprefixmo  27746  noinfprefixmo  27747  nosupno  27749  noinfno  27764  etasslt  27859  scutbdaybnd  27861  scutbdaybnd2  27862  addsproplem6  28008  negsproplem6  28066  mulsproplem13  28155  mulsproplem14  28156  mulsprop  28157  ax5seglem6  28950  fusgrfis  29348  wwlksnextfun  29919  umgr2wlkon  29971  connpconn  35241  cvmlift3lem2  35326  cvmlift3lem8  35332  ifscgr  36046  broutsideof3  36128  unblimceq0  36509  paddasslem10  39832  lhpexle2lem  40012  lhpexle3lem  40014  mpaaeu  43167  stoweidlem35  46055  stoweidlem56  46076  stoweidlem59  46079
  Copyright terms: Public domain W3C validator