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

Theorem mpanr2 702
Description: An inference based on modus ponens. (Contributed by NM, 3-May-1994.) (Proof shortened by Andrew Salmon, 7-May-2011.) (Proof shortened by Wolf Lammen, 7-Apr-2013.)
Hypotheses
Ref Expression
mpanr2.1 𝜒
mpanr2.2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
Assertion
Ref Expression
mpanr2 ((𝜑𝜓) → 𝜃)

Proof of Theorem mpanr2
StepHypRef Expression
1 mpanr2.1 . . 3 𝜒
21jctr 523 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 591 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 394
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 395
This theorem is referenced by:  fvreseq1  7047  op1steq  8038  fpmg  8887  pmresg  8889  pw2f1o  9102  pm54.43  10026  dfac2b  10155  ttukeylem6  10539  gruina  10843  muleqadd  11890  divdiv1  11958  addltmul  12481  elfzp1b  13613  elfzm1b  13614  expp1z  14112  expm1  14113  oddvdsnn0  19511  efgi0  19687  efgi1  19688  fiinbas  22899  opnneissb  23062  fclscf  23973  blssec  24385  iimulcl  24904  itg2lr  25704  blocnilem  30686  lnopmul  31849  opsqrlem6  32027  gsumle  32894  gsumvsca1  33025  gsumvsca2  33026  locfinreflem  33572  fvray  35868  fvline  35871  fneref  35965  poimirlem3  37227  poimirlem16  37240  fdc  37349  linepmap  39378  rmyeq0  42516
  Copyright terms: Public domain W3C validator