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

Theorem simplld 764
Description: Deduction form of simpll 763, 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  8787  lejoin1  18341  lemeet1  18355  reldir  18556  gexdvdsi  19492  lmhmlmod1  20788  pi1cpbl  24791  oppne1  28259  trgcopyeulem  28323  dfcgra2  28348  subupgr  28811  3trlond  29693  3pthond  29695  3spthond  29697  grpolid  30036  mgcf1  32425  mgccole1  32427  mgcmnt1  32429  mgcmnt2  32430  mgcf1olem1  32438  mgcf1olem2  32439  mgcf1o  32440  mfsdisj  34839  linethru  35429  rngoablo  37079  fourierdlem37  45158  fourierdlem48  45168  fourierdlem93  45213  fourierdlem94  45214  fourierdlem104  45224  fourierdlem112  45232  fourierdlem113  45233  dmmeasal  45466  meaf  45467  meaiuninclem  45494  omef  45510  ome0  45511  omedm  45513  hspmbllem3  45642
  Copyright terms: Public domain W3C validator