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

Theorem mpanr2 722
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 566 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 492 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:  fvreseq1  6482  op1steq  7378  fpmg  8051  pmresg  8053  pw2f1o  8232  pm54.43  9036  dfac2b  9163  dfac2OLD  9165  ttukeylem6  9548  gruina  9852  muleqadd  10883  divdiv1  10948  addltmul  11480  elfzp1b  12630  elfzm1b  12631  expp1z  13123  expm1  13124  oddvdsnn0  18183  efgi0  18353  efgi1  18354  fiinbas  20978  opnneissb  21140  fclscf  22050  blssec  22461  iimulcl  22957  itg2lr  23716  blocnilem  27989  lnopmul  29156  opsqrlem6  29334  gsumle  30109  gsumvsca1  30112  gsumvsca2  30113  locfinreflem  30237  fvray  32575  fvline  32578  fneref  32672  poimirlem3  33743  poimirlem16  33756  fdc  33872  linepmap  35582  rmyeq0  38040
  Copyright terms: Public domain W3C validator