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

Theorem simplld 808
Description: Deduction form of simpll 807, 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 477 . 2 (𝜑 → (𝜓𝜒))
32simpld 477 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:  lejoin1  17213  lemeet1  17227  reldir  17434  gexdvdsi  18198  lmhmlmod1  19235  oppne1  25832  trgcopyeulem  25896  dfcgra2  25920  subupgr  26378  3trlond  27325  3pthond  27327  3spthond  27329  grpolid  27679  mfsdisj  31754  linethru  32566  rngoablo  34020  fourierdlem37  40864  fourierdlem48  40874  fourierdlem93  40919  fourierdlem94  40920  fourierdlem104  40930  fourierdlem112  40938  fourierdlem113  40939  ismea  41171  dmmeasal  41172  meaf  41173  meaiuninclem  41200  omef  41216  ome0  41217  omedm  41219  hspmbllem3  41348
  Copyright terms: Public domain W3C validator