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

Theorem simplld 786
Description: Deduction form of simpll 785, 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 473 . 2 (𝜑 → (𝜓𝜒))
32simpld 473 1 (𝜑𝜓)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  lejoin1  16778  lemeet1  16792  reldir  16999  gexdvdsi  17764  lmhmlmod1  18797  oppne1  25348  trgcopyeulem  25412  dfcgra2  25436  constr3cyclp  25953  grpolid  26517  mfsdisj  30504  linethru  31233  rngoablo  32677  fourierdlem37  38838  fourierdlem48  38848  fourierdlem93  38893  fourierdlem94  38894  fourierdlem104  38904  fourierdlem112  38912  fourierdlem113  38913  ismea  39145  dmmeasal  39146  meaf  39147  meaiuninclem  39174  omef  39187  ome0  39188  omedm  39190  hspmbllem3  39319  subupgr  40510  3trlond  41339  3pthond  41341  3spthond  41343
  Copyright terms: Public domain W3C validator