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

Theorem mpan2i 709
 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 706 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:  tcwf  8629  cflecard  8958  sqrlem7  13837  setciso  16564  lsmss1  17902  sincosq1lem  24053  pjcompi  27915  mdsl1i  28564  dfon2lem3  30934  dfon2lem7  30938  tan2h  32571  dvasin  32666  ismrc  36282  nnsum4primes4  40205  nnsum4primesprm  40207  nnsum4primesgbe  40209  nnsum4primesle9  40211  rngciso  41774  rngcisoALTV  41786  ringciso  41825  ringcisoALTV  41849  aacllem  42356
 Copyright terms: Public domain W3C validator