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

Theorem simprld 770
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 496 . 2 (𝜑 → (𝜒𝜃))
32simpld 495 1 (𝜑𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  fpwwe2lem5  10529  fpwwe2lem6  10530  fpwwe2lem8  10532  canthnumlem  10542  canthp1lem2  10547  latcl2  18279  clatlem  18345  dirtr  18445  srglz  19892  lmodvsass  20294  lmghm  20439  evlssca  21445  mircgr  27444  dfcgra2  27617  mgcmnt1d  31699  mgcmnt2d  31700  mgcf1o  31705  ssmxidllem  32076  ssmxidl  32077  maxsta  33976  lbioc  43646  icccncfext  44023  stoweidlem37  44173  fourierdlem41  44284  fourierdlem48  44290  fourierdlem49  44291  fourierdlem74  44316  fourierdlem75  44317  salgencl  44468  salgenuni  44473  issalgend  44474  smfaddlem1  44899
  Copyright terms: Public domain W3C validator