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

Theorem simplrd 768
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 493 . 2 (𝜑 → (𝜓𝜒))
32simprd 494 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  erinxp  8810  fpwwe2lem5  10660  fpwwe2lem6  10661  fpwwe2lem8  10663  lejoin2  18380  lemeet2  18394  dirdm  18595  dirref  18596  lmhmlmod2  20929  pi1cpbl  25015  pntlemr  27580  oppne2  28618  dfcgra2  28706  mgcf2  32805  mgccole2  32807  mgcmnt1  32808  mgcmnt2  32809  mgcf1olem1  32817  mgcf1olem2  32818  mgcf1o  32819  erlcl2  33051  erler  33055  mtyf2  35289  ioodvbdlimc1lem2  45455  ioodvbdlimc2lem  45457  fourierdlem48  45677  fourierdlem76  45705  fourierdlem80  45709  fourierdlem93  45722  fourierdlem94  45723  fourierdlem104  45733  fourierdlem113  45742  mea0  45977  meaiunlelem  45991  meaiuninclem  46003  omessle  46021  omedm  46022  carageniuncllem2  46045  hspmbllem3  46151
  Copyright terms: Public domain W3C validator