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

Theorem simprrd 792
Description: Deduction form of simprr 791, eliminating a double conjunct. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
Hypothesis
Ref Expression
simprrd.1 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
Assertion
Ref Expression
simprrd (𝜑𝜃)

Proof of Theorem simprrd
StepHypRef Expression
1 simprrd.1 . . 3 (𝜑 → (𝜓 ∧ (𝜒𝜃)))
21simprd 477 . 2 (𝜑 → (𝜒𝜃))
32simprd 477 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:  fpwwe2lem3  9307  uzind  11297  latcl2  16813  clatlem  16876  dirge  17002  srgrz  18291  lmodvs1  18656  lmhmsca  18793  evlsvar  19286  mirbtwn  25267  dfcgra2  25435  trlonistrl  25835  pthonispth  25870  spthonisspth  25878  numclwwlk2lem1  26391  axtgupdim2OLD  29801  mvtinf  30508  rngoid  32670  rngoideu  32671  rngorn1eq  32702  rngomndo  32703  mzpcl34  36111  icccncfext  38573  fourierdlem12  38812  fourierdlem34  38834  fourierdlem41  38841  fourierdlem48  38847  fourierdlem49  38848  fourierdlem74  38873  fourierdlem75  38874  fourierdlem76  38875  fourierdlem89  38888  fourierdlem91  38890  fourierdlem92  38891  fourierdlem94  38893  fourierdlem113  38912  sssalgen  39029  issalgend  39032  smfaddlem1  39449  3trlond  41338  3pthond  41340  3spthond  41342
  Copyright terms: Public domain W3C validator