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

Theorem mpanr2 704
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 524 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 593 1 ((𝜑𝜓) → 𝜃)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395
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 207  df-an 396
This theorem is referenced by:  fvreseq1  6984  op1steq  7977  fpmg  8806  pmresg  8808  pw2f1o  9010  pm54.43  9913  dfac2b  10041  ttukeylem6  10424  gruina  10729  muleqadd  11781  divdiv1  11852  addltmul  12377  elfzp1b  13517  elfzm1b  13518  expp1z  14034  expm1  14035  oddvdsnn0  19473  efgi0  19649  efgi1  19650  gsumle  20074  fiinbas  22896  opnneissb  23058  fclscf  23969  blssec  24379  iimulcl  24889  itg2lr  25687  blocnilem  30879  lnopmul  32042  opsqrlem6  32220  gsumvsca1  33308  gsumvsca2  33309  locfinreflem  33997  fvray  36335  fvline  36338  fneref  36544  poimirlem3  37824  poimirlem16  37837  fdc  37946  linepmap  40035  rmyeq0  43195  omssaxinf2  45229
  Copyright terms: Public domain W3C validator