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

Theorem simplld 790
Description: Deduction form of simpll 789, 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 475 . 2 (𝜑 → (𝜓𝜒))
32simpld 475 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 386
This theorem is referenced by:  lejoin1  16952  lemeet1  16966  reldir  17173  gexdvdsi  17938  lmhmlmod1  18973  oppne1  25567  trgcopyeulem  25631  dfcgra2  25655  subupgr  26106  3trlond  26933  3pthond  26935  3spthond  26937  grpolid  27258  mfsdisj  31208  linethru  31955  rngoablo  33378  fourierdlem37  39698  fourierdlem48  39708  fourierdlem93  39753  fourierdlem94  39754  fourierdlem104  39764  fourierdlem112  39772  fourierdlem113  39773  ismea  40005  dmmeasal  40006  meaf  40007  meaiuninclem  40034  omef  40047  ome0  40048  omedm  40050  hspmbllem3  40179
  Copyright terms: Public domain W3C validator