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

Theorem mpan2i 677
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2i.1 𝜒
mpan2i.2 (𝜑 → ((𝜓𝜒) → 𝜃))
Assertion
Ref Expression
mpan2i (𝜑 → (𝜓𝜃))

Proof of Theorem mpan2i
StepHypRef Expression
1 mpan2i.1 . . 3 𝜒
21a1i 11 . 2 (𝜑𝜒)
3 mpan2i.2 . 2 (𝜑 → ((𝜓𝜒) → 𝜃))
42, 3mpan2d 674 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 383
This theorem is referenced by:  tcwf  8910  cflecard  9277  sqrlem7  14193  setciso  16944  lsmss1  18282  sincosq1lem  24466  pjcompi  28867  mdsl1i  29516  dfon2lem3  32022  dfon2lem7  32026  tan2h  33730  dvasin  33824  ismrc  37787  nnsum4primes4  42202  nnsum4primesprm  42204  nnsum4primesgbe  42206  nnsum4primesle9  42208  rngciso  42507  rngcisoALTV  42519  ringciso  42558  ringcisoALTV  42582  aacllem  43075
  Copyright terms: Public domain W3C validator