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

Theorem mpan2i 680
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 677 1 (𝜑 → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  tcwf  8993  cflecard  9360  sqrlem7  14212  setciso  16945  lsmss1  18280  sincosq1lem  24464  pjcompi  28859  mdsl1i  29508  dfon2lem3  32010  dfon2lem7  32014  tan2h  33714  dvasin  33808  ismrc  37766  nnsum4primes4  42252  nnsum4primesprm  42254  nnsum4primesgbe  42256  nnsum4primesle9  42258  rngciso  42550  rngcisoALTV  42562  ringciso  42601  ringcisoALTV  42625  aacllem  43118
  Copyright terms: Public domain W3C validator