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

Theorem mp2and 429
Description: A deduction based on modus ponens. (Contributed by NM, 12-Dec-2004.)
Hypotheses
Ref Expression
mp2and.1  |-  ( ph  ->  ps )
mp2and.2  |-  ( ph  ->  ch )
mp2and.3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
Assertion
Ref Expression
mp2and  |-  ( ph  ->  th )

Proof of Theorem mp2and
StepHypRef Expression
1 mp2and.2 . 2  |-  ( ph  ->  ch )
2 mp2and.1 . . 3  |-  ( ph  ->  ps )
3 mp2and.3 . . 3  |-  ( ph  ->  ( ( ps  /\  ch )  ->  th )
)
42, 3mpand 425 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 13 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  tfisi  4471  tfr0dm  6187  tfr1onlemaccex  6213  tfrcllemaccex  6226  ertrd  6413  th3qlem1  6499  findcard2  6751  findcard2s  6752  diffifi  6756  fimax2gtrilemstep  6762  fidcenumlemrk  6810  fidcenumlemr  6811  isbth  6823  ltbtwnnqq  7191  prarloclemarch2  7195  addlocprlemeqgt  7308  addnqprlemrl  7333  addnqprlemru  7334  mulnqprlemrl  7349  mulnqprlemru  7350  ltexprlemrl  7386  ltexprlemru  7388  addcanprleml  7390  addcanprlemu  7391  recexprlemloc  7407  recexprlem1ssu  7410  cauappcvgprlemladdfl  7431  caucvgprlemloc  7451  caucvgprprlemloccalc  7460  letrd  7854  lelttrd  7855  lttrd  7856  ltletrd  8153  le2addd  8293  le2subd  8294  ltleaddd  8295  leltaddd  8296  lt2subd  8298  ltmul12a  8586  lediv12a  8620  lemul12ad  8668  lemul12bd  8669  lt2halvesd  8935  uzind  9130  uztrn  9310  xrlttrd  9560  xrlelttrd  9561  xrltletrd  9562  xrletrd  9563  ixxss1  9655  ixxss2  9656  ixxss12  9657  fldiv4p1lem1div2  10046  faclbnd3  10457  abs3lemd  10941  xrbdtri  11013  modfsummod  11195  mertenslemi1  11272  sin01gt0  11395  cos01gt0  11396  sin02gt0  11397  dvds2subd  11456  zsupcllemex  11566  zssinfcl  11568  bezoutlemstep  11612  mulgcd  11631  gcddvdslcm  11681  lcmgcdeq  11691  mulgcddvds  11702  rpmulgcd2  11703  rpdvds  11707  divgcdcoprmex  11710  rpexp  11758  phimullem  11828  exmidunben  11866  lmtopcnp  12346  blin2  12528  xmetxp  12603  tgqioo  12643  cncfmptid  12679  negcncf  12684  limcimolemlt  12729  sinq12gt0  12838
  Copyright terms: Public domain W3C validator