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

Theorem simprrd 793
 Description: Deduction form of simprr 792, 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 478 . 2 (𝜑 → (𝜒𝜃))
32simprd 478 1 (𝜑𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 383 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 196  df-an 385 This theorem is referenced by:  fpwwe2lem3  9334  uzind  11345  latcl2  16871  clatlem  16934  dirge  17060  srgrz  18349  lmodvs1  18714  lmhmsca  18851  evlsvar  19344  mirbtwn  25353  dfcgra2  25521  trlonistrl  26073  pthonispth  26108  spthonisspth  26116  numclwwlk2lem1  26629  axtgupdim2OLD  29999  mvtinf  30706  rngoid  32871  rngoideu  32872  rngorn1eq  32903  rngomndo  32904  mzpcl34  36312  icccncfext  38773  fourierdlem12  39012  fourierdlem34  39034  fourierdlem41  39041  fourierdlem48  39047  fourierdlem49  39048  fourierdlem74  39073  fourierdlem75  39074  fourierdlem76  39075  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem94  39093  fourierdlem113  39112  sssalgen  39229  issalgend  39232  smfaddlem1  39649  3trlond  41340  3pthond  41342  3spthond  41344
 Copyright terms: Public domain W3C validator