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

Theorem mpan2i 675
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  |-  ch
mpan2i.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpan2i  |-  ( ph  ->  ( ps  ->  th )
)

Proof of Theorem mpan2i
StepHypRef Expression
1 mpan2i.1 . . 3  |-  ch
21a1i 11 . 2  |-  ( ph  ->  ch )
3 mpan2i.2 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpan2d 672 1  |-  ( ph  ->  ( ps  ->  th )
)
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367
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 185  df-an 369
This theorem is referenced by:  tcwf  8333  cflecard  8665  sqrlem7  13231  setciso  15694  lsmss1  17008  sincosq1lem  23182  pjcompi  27004  mdsl1i  27653  dfon2lem3  30004  dfon2lem7  30008  tan2h  31419  dvasin  31474  ismrc  34995  nnsum4primes4  37837  nnsum4primesprm  37839  nnsum4primesgbe  37841  nnsum4primesle9  37843  rngciso  38301  rngcisoALTV  38313  ringciso  38352  ringcisoALTV  38376  aacllem  38860
  Copyright terms: Public domain W3C validator