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

Theorem simprrd 764
Description: Deduction form of simprr 763, 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 491 . 2 (𝜑 → (𝜒𝜃))
32simprd 491 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 386
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 199  df-an 387
This theorem is referenced by:  fpwwe2lem3  9790  uzind  11821  latcl2  17434  clatlem  17497  dirge  17623  srgrz  18913  lmodvs1  19283  lmhmsca  19425  evlsvar  19919  mirbtwn  26009  dfcgra2  26178  3trlond  27576  3pthond  27578  3spthond  27580  axtgupdim2OLD  31348  mvtinf  32051  rngoid  34325  rngoideu  34326  rngorn1eq  34357  rngomndo  34358  mzpcl34  38254  icccncfext  41028  fourierdlem12  41263  fourierdlem34  41285  fourierdlem41  41292  fourierdlem48  41298  fourierdlem49  41299  fourierdlem74  41324  fourierdlem75  41325  fourierdlem76  41326  fourierdlem89  41339  fourierdlem91  41341  fourierdlem92  41342  fourierdlem94  41344  fourierdlem113  41363  sssalgen  41477  issalgend  41480  smfaddlem1  41898
  Copyright terms: Public domain W3C validator