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

Theorem simprld 772
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 495 . 2 (𝜑 → (𝜒𝜃))
32simpld 494 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  canthnumlem  10688  canthp1lem2  10693  latcl2  18481  clatlem  18547  dirtr  18647  srglz  20205  lmodvsass  20885  lmghm  21030  evlssca  22113  mircgr  28665  dfcgra2  28838  mgcmnt1d  32987  mgcmnt2d  32988  mgcf1o  32993  ssmxidllem  33501  ssmxidl  33502  maxsta  35559  lbioc  45526  icccncfext  45902  stoweidlem37  46052  fourierdlem41  46163  fourierdlem48  46169  fourierdlem49  46170  fourierdlem74  46195  fourierdlem75  46196  salgencl  46347  salgenuni  46352  issalgend  46353  smfaddlem1  46778
  Copyright terms: Public domain W3C validator