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

Theorem simprrd 771
Description: Deduction form of simprr 770, 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 495 . 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 206  df-an 396
This theorem is referenced by:  fpwwe2lem3  10630  uzind  12658  latcl2  18401  clatlem  18467  dirge  18568  srgrz  20112  lmodvs1  20736  lmhmsca  20878  evlsvar  21995  mirbtwn  28417  dfcgra2  28589  3trlond  29935  3pthond  29937  3spthond  29939  ssmxidllem  33095  ssmxidl  33096  axtgupdim2ALTV  34209  mvtinf  35074  rngoid  37283  rngoideu  37284  rngorn1eq  37315  rngomndo  37316  fzne2d  41362  mzpcl34  42052  icccncfext  45180  fourierdlem12  45412  fourierdlem34  45434  fourierdlem41  45441  fourierdlem48  45447  fourierdlem49  45448  fourierdlem74  45473  fourierdlem75  45474  fourierdlem76  45475  fourierdlem89  45488  fourierdlem91  45490  fourierdlem92  45491  fourierdlem94  45493  fourierdlem113  45512  sssalgen  45628  issalgend  45631  smfaddlem1  46056
  Copyright terms: Public domain W3C validator