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

Theorem simprrd 814
 Description: Deduction form of simprr 813, 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 482 . 2 (𝜑 → (𝜒𝜃))
32simprd 482 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 197  df-an 385 This theorem is referenced by:  fpwwe2lem3  9647  uzind  11661  latcl2  17249  clatlem  17312  dirge  17438  srgrz  18726  lmodvs1  19093  lmhmsca  19232  evlsvar  19725  mirbtwn  25752  dfcgra2  25920  3trlond  27325  3pthond  27327  3spthond  27329  axtgupdim2OLD  31055  mvtinf  31759  rngoid  34014  rngoideu  34015  rngorn1eq  34046  rngomndo  34047  mzpcl34  37796  icccncfext  40603  fourierdlem12  40839  fourierdlem34  40861  fourierdlem41  40868  fourierdlem48  40874  fourierdlem49  40875  fourierdlem74  40900  fourierdlem75  40901  fourierdlem76  40902  fourierdlem89  40915  fourierdlem91  40917  fourierdlem92  40918  fourierdlem94  40920  fourierdlem113  40939  sssalgen  41056  issalgend  41059  smfaddlem1  41477
 Copyright terms: Public domain W3C validator