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

Theorem simplld 784
Description: Deduction form of simpll 783, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
simplld.1 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
Assertion
Ref Expression
simplld (𝜑𝜓)

Proof of Theorem simplld
StepHypRef Expression
1 simplld.1 . . 3 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
21simpld 490 . 2 (𝜑 → (𝜓𝜒))
32simpld 490 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  erinxp  8086  lejoin1  17365  lemeet1  17379  reldir  17586  gexdvdsi  18349  lmhmlmod1  19392  pi1cpbl  23213  oppne1  26050  trgcopyeulem  26114  dfcgra2  26138  subupgr  26584  3trlond  27538  3pthond  27540  3spthond  27542  grpolid  27915  mfsdisj  31982  linethru  32788  rngoablo  34242  fourierdlem37  41148  fourierdlem48  41158  fourierdlem93  41203  fourierdlem94  41204  fourierdlem104  41214  fourierdlem112  41222  fourierdlem113  41223  ismea  41452  dmmeasal  41453  meaf  41454  meaiuninclem  41481  omef  41497  ome0  41498  omedm  41500  hspmbllem3  41629
  Copyright terms: Public domain W3C validator