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

Theorem simplrd 810
 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 477 . 2 (𝜑 → (𝜓𝜒))
32simprd 482 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 197  df-an 385 This theorem is referenced by:  dfcgra2  25841  mtyf2  31676  ioodvbdlimc1lem2  40567  ioodvbdlimc2lem  40569  fourierdlem48  40791  fourierdlem76  40819  fourierdlem80  40823  fourierdlem93  40836  fourierdlem94  40837  fourierdlem104  40847  fourierdlem113  40856  ismea  41088  mea0  41091  meaiunlelem  41105  meaiuninclem  41117  omessle  41135  omedm  41136  carageniuncllem2  41159  hspmbllem3  41265
 Copyright terms: Public domain W3C validator