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

Theorem simplld 787
 Description: Deduction form of simpll 786, 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 474 . 2 (𝜑 → (𝜓𝜒))
32simpld 474 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 196  df-an 385 This theorem is referenced by:  lejoin1  16835  lemeet1  16849  reldir  17056  gexdvdsi  17821  lmhmlmod1  18854  oppne1  25433  trgcopyeulem  25497  dfcgra2  25521  constr3cyclp  26190  grpolid  26754  mfsdisj  30701  linethru  31430  rngoablo  32877  fourierdlem37  39037  fourierdlem48  39047  fourierdlem93  39092  fourierdlem94  39093  fourierdlem104  39103  fourierdlem112  39111  fourierdlem113  39112  ismea  39344  dmmeasal  39345  meaf  39346  meaiuninclem  39373  omef  39386  ome0  39387  omedm  39389  hspmbllem3  39518  subupgr  40511  3trlond  41340  3pthond  41342  3spthond  41344
 Copyright terms: Public domain W3C validator