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

Theorem mpan2i 693
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 690 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 208  df-an 397
This theorem is referenced by:  tcwf  9301  cflecard  9664  sqrlem7  14598  setciso  17341  lsmss1  18711  sincosq1lem  24998  pjcompi  29363  mdsl1i  30012  dfon2lem3  32914  dfon2lem7  32918  tan2h  34751  dvasin  34845  ismrc  39163  nnsum4primes4  43786  nnsum4primesprm  43788  nnsum4primesgbe  43790  nnsum4primesle9  43792  rngciso  44085  rngcisoALTV  44097  ringciso  44136  ringcisoALTV  44160  aacllem  44734
  Copyright terms: Public domain W3C validator