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

Theorem simplrd 757
Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
simplrd.1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
Assertion
Ref Expression
simplrd (𝜑𝜒)

Proof of Theorem simplrd
StepHypRef Expression
1 simplrd.1 . . 3 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
21simpld 487 . 2 (𝜑 → (𝜓𝜒))
32simprd 488 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 387
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 199  df-an 388
This theorem is referenced by:  erinxp  8163  fpwwe2lem6  9847  fpwwe2lem7  9848  fpwwe2lem9  9850  lejoin2  17471  lemeet2  17485  dirdm  17692  dirref  17693  lmhmlmod2  19516  pi1cpbl  23341  pntlemr  25870  oppne2  26220  dfcgra2  26308  mtyf2  32258  ioodvbdlimc1lem2  41593  ioodvbdlimc2lem  41595  fourierdlem48  41816  fourierdlem76  41844  fourierdlem80  41848  fourierdlem93  41861  fourierdlem94  41862  fourierdlem104  41872  fourierdlem113  41881  mea0  42113  meaiunlelem  42127  meaiuninclem  42139  omessle  42157  omedm  42158  carageniuncllem2  42181  hspmbllem3  42287
  Copyright terms: Public domain W3C validator