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

Theorem simplld 767
 Description: Deduction form of simpll 766, 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 498 . 2 (𝜑 → (𝜓𝜒))
32simpld 498 1 (𝜑𝜓)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399 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 210  df-an 400 This theorem is referenced by:  erinxp  8354  lejoin1  17611  lemeet1  17625  reldir  17832  gexdvdsi  18697  lmhmlmod1  19791  pi1cpbl  23638  oppne1  26524  trgcopyeulem  26588  dfcgra2  26613  subupgr  27066  3trlond  27947  3pthond  27949  3spthond  27951  grpolid  28288  mgcf1  30667  mgccole1  30669  mcgmnt1  30671  mcgmnt2  30672  mfsdisj  32815  linethru  33632  rngoablo  35246  fourierdlem37  42628  fourierdlem48  42638  fourierdlem93  42683  fourierdlem94  42684  fourierdlem104  42694  fourierdlem112  42702  fourierdlem113  42703  dmmeasal  42933  meaf  42934  meaiuninclem  42961  omef  42977  ome0  42978  omedm  42980  hspmbllem3  43109
 Copyright terms: Public domain W3C validator