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

Theorem simplrd 769
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 496 . 2 (𝜑 → (𝜓𝜒))
32simprd 497 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  erinxp  8785  fpwwe2lem5  10630  fpwwe2lem6  10631  fpwwe2lem8  10633  lejoin2  18338  lemeet2  18352  dirdm  18553  dirref  18554  lmhmlmod2  20643  pi1cpbl  24560  pntlemr  27105  oppne2  27993  dfcgra2  28081  mgcf2  32159  mgccole2  32161  mgcmnt1  32162  mgcmnt2  32163  mgcf1olem1  32171  mgcf1olem2  32172  mgcf1o  32173  mtyf2  34542  ioodvbdlimc1lem2  44648  ioodvbdlimc2lem  44650  fourierdlem48  44870  fourierdlem76  44898  fourierdlem80  44902  fourierdlem93  44915  fourierdlem94  44916  fourierdlem104  44926  fourierdlem113  44935  mea0  45170  meaiunlelem  45184  meaiuninclem  45196  omessle  45214  omedm  45215  carageniuncllem2  45238  hspmbllem3  45344
  Copyright terms: Public domain W3C validator