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

Theorem mpanr2 716
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 563 . 2 (𝜓 → (𝜓𝜒))
3 mpanr2.2 . 2 ((𝜑 ∧ (𝜓𝜒)) → 𝜃)
42, 3sylan2 490 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 196  df-an 385
This theorem is referenced by:  fvreseq1  6211  op1steq  7079  fpmg  7747  pmresg  7749  pw2f1o  7928  pm54.43  8687  dfac2  8814  ttukeylem6  9197  gruina  9497  muleqadd  10523  divdiv1  10588  addltmul  11118  elfzp1b  12244  elfzm1b  12245  expp1z  12729  expm1  12730  oddvdsnn0  17735  efgi0  17905  efgi1  17906  fiinbas  20515  opnneissb  20676  fclscf  21587  blssec  21998  iimulcl  22492  itg2lr  23248  blocnilem  26837  lnopmul  28004  opsqrlem6  28182  gsumle  28904  gsumvsca1  28907  gsumvsca2  28908  locfinreflem  29029  fvray  31212  fvline  31215  fneref  31309  poimirlem3  32376  poimirlem16  32389  fdc  32505  linepmap  33873  rmyeq0  36332
  Copyright terms: Public domain W3C validator