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

Theorem simplld 766
Description: Deduction form of simpll 765, 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 493 . 2 (𝜑 → (𝜓𝜒))
32simpld 493 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 206  df-an 395
This theorem is referenced by:  erinxp  8810  lejoin1  18379  lemeet1  18393  reldir  18594  gexdvdsi  19550  lmhmlmod1  20930  pi1cpbl  25015  oppne1  28617  trgcopyeulem  28681  dfcgra2  28706  subupgr  29172  3trlond  30055  3pthond  30057  3spthond  30059  grpolid  30398  mgcf1  32804  mgccole1  32806  mgcmnt1  32808  mgcmnt2  32809  mgcf1olem1  32817  mgcf1olem2  32818  mgcf1o  32819  erlcl1  33050  erler  33055  mfsdisj  35288  linethru  35877  rngoablo  37509  fourierdlem37  45667  fourierdlem48  45677  fourierdlem93  45722  fourierdlem94  45723  fourierdlem104  45733  fourierdlem112  45741  fourierdlem113  45742  dmmeasal  45975  meaf  45976  meaiuninclem  46003  omef  46019  ome0  46020  omedm  46022  hspmbllem3  46151
  Copyright terms: Public domain W3C validator