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

Theorem simplrd 789
 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 474 . 2 (𝜑 → (𝜓𝜒))
32simprd 478 1 (𝜑𝜒)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  dfcgra2  25521  ioodvbdlimc1lem2  38822  ioodvbdlimc2lem  38824  fourierdlem48  39047  fourierdlem76  39075  fourierdlem80  39079  fourierdlem93  39092  fourierdlem94  39093  fourierdlem104  39103  fourierdlem113  39112  ismea  39344  mea0  39347  meaiunlelem  39361  meaiuninclem  39373  omessle  39388  omedm  39389  carageniuncllem2  39412  hspmbllem3  39518  isclwwlksng  41196
 Copyright terms: Public domain W3C validator