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

Theorem simprld 771
 Description: Deduction eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
simprld.1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Assertion
Ref Expression
simprld (𝜑𝜒)

Proof of Theorem simprld
StepHypRef Expression
1 simprld.1 . . 3 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
21simprd 499 . 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:  fpwwe2lem6  10050  fpwwe2lem7  10051  fpwwe2lem9  10053  canthnumlem  10063  canthp1lem2  10068  latcl2  17654  clatlem  17717  dirtr  17842  srglz  19274  lmodvsass  19656  lmghm  19800  evlssca  20765  mircgr  26455  dfcgra2  26628  ssmxidllem  31053  ssmxidl  31054  maxsta  32915  lbioc  42147  icccncfext  42526  stoweidlem37  42676  fourierdlem41  42787  fourierdlem48  42793  fourierdlem49  42794  fourierdlem74  42819  fourierdlem75  42820  salgencl  42969  salgenuni  42974  issalgend  42975  smfaddlem1  43393
 Copyright terms: Public domain W3C validator