ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpani Unicode version

Theorem mpani 421
Description: An inference based on modus ponens. (Contributed by NM, 10-Apr-1994.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpani.1  |-  ps
mpani.2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mpani  |-  ( ph  ->  ( ch  ->  th )
)

Proof of Theorem mpani
StepHypRef Expression
1 mpani.1 . . 3  |-  ps
21a1i 9 . 2  |-  ( ph  ->  ps )
3 mpani.2 . 2  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 420 1  |-  ( ph  ->  ( ch  ->  th )
)
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  mp2ani  423  mulgt1  8078  recgt1i  8113  recreclt  8115  nngt0  8201  nnrecgt0  8213  elnnnn0c  8470  elnnz1  8525  recnz  8591  uz3m2nn  8812  ledivge1le  8954  expubnd  9700  expnbnd  9763  expnlbnd  9764  oddge22np1  10506  dvdsnprmd  10732
  Copyright terms: Public domain W3C validator