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

Theorem mpanr2 719
 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 564 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 491 1 ((𝜑𝜓) → 𝜃)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 384 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 386 This theorem is referenced by:  fvreseq1  6284  op1steq  7170  fpmg  7843  pmresg  7845  pw2f1o  8025  pm54.43  8786  dfac2  8913  ttukeylem6  9296  gruina  9600  muleqadd  10631  divdiv1  10696  addltmul  11228  elfzp1b  12374  elfzm1b  12375  expp1z  12865  expm1  12866  oddvdsnn0  17903  efgi0  18073  efgi1  18074  fiinbas  20696  opnneissb  20858  fclscf  21769  blssec  22180  iimulcl  22676  itg2lr  23437  blocnilem  27547  lnopmul  28714  opsqrlem6  28892  gsumle  29606  gsumvsca1  29609  gsumvsca2  29610  locfinreflem  29731  fvray  31943  fvline  31946  fneref  32040  poimirlem3  33083  poimirlem16  33096  fdc  33212  linepmap  34580  rmyeq0  37039
 Copyright terms: Public domain W3C validator