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

Theorem mpan2i 708
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 705 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 195  df-an 384
This theorem is referenced by:  tcwf  8606  cflecard  8935  sqrlem7  13785  setciso  16512  lsmss1  17850  sincosq1lem  23997  pjcompi  27708  mdsl1i  28357  dfon2lem3  30727  dfon2lem7  30731  tan2h  32354  dvasin  32449  ismrc  36065  nnsum4primes4  39989  nnsum4primesprm  39991  nnsum4primesgbe  39993  nnsum4primesle9  39995  rngciso  41755  rngcisoALTV  41767  ringciso  41806  ringcisoALTV  41830  aacllem  42298
  Copyright terms: Public domain W3C validator