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

Theorem simprr3 1215
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 1130 . 2 ((𝜑𝜓𝜒) → 𝜒)
21ad2antll 725 1 ((𝜏 ∧ (𝜃 ∧ (𝜑𝜓𝜒))) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  el2xptp0  7725  icodiamlt  14783  psgnunilem2  18552  srgbinom  19224  psgndiflemA  20673  haust1  21888  cnhaus  21890  isreg2  21913  llynlly  22013  restnlly  22018  llyrest  22021  llyidm  22024  nllyidm  22025  cldllycmp  22031  txlly  22172  txnlly  22173  pthaus  22174  txhaus  22183  txkgen  22188  xkohaus  22189  xkococnlem  22195  cmetcaulem  23818  itg2add  24287  ulmdvlem3  24917  ax5seglem6  26647  fusgrfis  27039  wwlksnextfun  27603  umgr2wlkon  27656  connpconn  32379  cvmlift3lem2  32464  cvmlift3lem8  32470  noprefixmo  33099  nosupno  33100  scutbdaybnd  33172  ifscgr  33402  broutsideof3  33484  unblimceq0  33743  paddasslem10  36845  lhpexle2lem  37025  lhpexle3lem  37027  mpaaeu  39628  stoweidlem35  42197  stoweidlem56  42218  stoweidlem59  42221
  Copyright terms: Public domain W3C validator