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

Theorem simprrd 796
Description: Deduction form of simprr 795, 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 479 . 2 (𝜑 → (𝜒𝜃))
32simprd 479 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 197  df-an 386
This theorem is referenced by:  fpwwe2lem3  9415  uzind  11429  latcl2  16988  clatlem  17051  dirge  17177  srgrz  18466  lmodvs1  18831  lmhmsca  18970  evlsvar  19463  mirbtwn  25487  dfcgra2  25655  3trlond  26933  3pthond  26935  3spthond  26937  axtgupdim2OLD  30506  mvtinf  31213  rngoid  33372  rngoideu  33373  rngorn1eq  33404  rngomndo  33405  mzpcl34  36813  icccncfext  39435  fourierdlem12  39673  fourierdlem34  39695  fourierdlem41  39702  fourierdlem48  39708  fourierdlem49  39709  fourierdlem74  39734  fourierdlem75  39735  fourierdlem76  39736  fourierdlem89  39749  fourierdlem91  39751  fourierdlem92  39752  fourierdlem94  39754  fourierdlem113  39773  sssalgen  39890  issalgend  39893  smfaddlem1  40308
  Copyright terms: Public domain W3C validator