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

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

Proof of Theorem simplrd
StepHypRef Expression
1 simplrd.1 . . 3 (𝜑 → ((𝜓𝜒) ∧ 𝜃))
21simpld 494 . 2 (𝜑 → (𝜓𝜒))
32simprd 495 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:  erinxp  8831  fpwwe2lem5  10675  fpwwe2lem6  10676  fpwwe2lem8  10678  lejoin2  18430  lemeet2  18444  dirdm  18645  dirref  18646  lmhmlmod2  21031  pi1cpbl  25077  pntlemr  27646  oppne2  28750  dfcgra2  28838  mgcf2  32979  mgccole2  32981  mgcmnt1  32982  mgcmnt2  32983  mgcf1olem1  32991  mgcf1olem2  32992  mgcf1o  32993  erlcl2  33265  erler  33269  mtyf2  35556  ioodvbdlimc1lem2  45947  ioodvbdlimc2lem  45949  fourierdlem48  46169  fourierdlem76  46197  fourierdlem80  46201  fourierdlem93  46214  fourierdlem94  46215  fourierdlem104  46225  fourierdlem113  46234  mea0  46469  meaiunlelem  46483  meaiuninclem  46495  omessle  46513  omedm  46514  carageniuncllem2  46537  hspmbllem3  46643  uprcl5  48944
  Copyright terms: Public domain W3C validator