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

Theorem simprrd 773
Description: Deduction form of simprr 772, 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 499 . 2 (𝜑 → (𝜒𝜃))
32simprd 499 1 (𝜑𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  fpwwe2lem3  10032  uzind  12052  latcl2  17637  clatlem  17700  dirge  17826  srgrz  19255  lmodvs1  19638  lmhmsca  19778  evlsvar  20279  mirbtwn  26431  dfcgra2  26603  3trlond  27937  3pthond  27939  3spthond  27941  ssmxidllem  30989  ssmxidl  30990  axtgupdim2ALTV  31947  mvtinf  32810  rngoid  35226  rngoideu  35227  rngorn1eq  35258  rngomndo  35259  mzpcl34  39483  icccncfext  42352  fourierdlem12  42584  fourierdlem34  42606  fourierdlem41  42613  fourierdlem48  42619  fourierdlem49  42620  fourierdlem74  42645  fourierdlem75  42646  fourierdlem76  42647  fourierdlem89  42660  fourierdlem91  42662  fourierdlem92  42663  fourierdlem94  42665  fourierdlem113  42684  sssalgen  42798  issalgend  42801  smfaddlem1  43219
  Copyright terms: Public domain W3C validator