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 498 . 2 (𝜑 → (𝜓𝜒))
32simprd 499 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  erinxp  8358  fpwwe2lem6  10046  fpwwe2lem7  10047  fpwwe2lem9  10049  lejoin2  17614  lemeet2  17628  dirdm  17835  dirref  17836  lmhmlmod2  19795  pi1cpbl  23647  pntlemr  26184  oppne2  26534  dfcgra2  26622  mgcf2  30681  mgccole2  30683  mcgmnt1  30684  mcgmnt2  30685  mtyf2  32872  ioodvbdlimc1lem2  42514  ioodvbdlimc2lem  42516  fourierdlem48  42736  fourierdlem76  42764  fourierdlem80  42768  fourierdlem93  42781  fourierdlem94  42782  fourierdlem104  42792  fourierdlem113  42801  mea0  43033  meaiunlelem  43047  meaiuninclem  43059  omessle  43077  omedm  43078  carageniuncllem2  43101  hspmbllem3  43207
  Copyright terms: Public domain W3C validator