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  7058  op1steq  8059  fpmg  8909  pmresg  8911  pw2f1o  9118  pm54.43  10042  dfac2b  10172  ttukeylem6  10555  gruina  10859  muleqadd  11908  divdiv1  11979  addltmul  12504  elfzp1b  13642  elfzm1b  13643  expp1z  14153  expm1  14154  oddvdsnn0  19563  efgi0  19739  efgi1  19740  fiinbas  22960  opnneissb  23123  fclscf  24034  blssec  24446  iimulcl  24967  itg2lr  25766  blocnilem  30824  lnopmul  31987  opsqrlem6  32165  gsumle  33102  gsumvsca1  33233  gsumvsca2  33234  locfinreflem  33840  fvray  36143  fvline  36146  fneref  36352  poimirlem3  37631  poimirlem16  37644  fdc  37753  linepmap  39778  rmyeq0  42970  omssaxinf2  45010
  Copyright terms: Public domain W3C validator