MPE Home 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