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

Theorem mp2and 433
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 429 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 13 1  |-  ( ph  ->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  tfisi  4583  tfr0dm  6317  tfr1onlemaccex  6343  tfrcllemaccex  6356  ertrd  6545  th3qlem1  6631  findcard2  6883  findcard2s  6884  diffifi  6888  fimax2gtrilemstep  6894  fidcenumlemrk  6947  fidcenumlemr  6948  isbth  6960  cc2lem  7253  ltbtwnnqq  7402  prarloclemarch2  7406  addlocprlemeqgt  7519  addnqprlemrl  7544  addnqprlemru  7545  mulnqprlemrl  7560  mulnqprlemru  7561  ltexprlemrl  7597  ltexprlemru  7599  addcanprleml  7601  addcanprlemu  7602  recexprlemloc  7618  recexprlem1ssu  7621  cauappcvgprlemladdfl  7642  caucvgprlemloc  7662  caucvgprprlemloccalc  7671  letrd  8068  lelttrd  8069  lttrd  8070  ltletrd  8367  le2addd  8507  le2subd  8508  ltleaddd  8509  leltaddd  8510  lt2subd  8512  ltmul12a  8803  lediv12a  8837  lemul12ad  8885  lemul12bd  8886  lt2halvesd  9152  uzind  9350  uztrn  9530  xrlttrd  9793  xrlelttrd  9794  xrltletrd  9795  xrletrd  9796  ixxss1  9888  ixxss2  9889  ixxss12  9890  fldiv4p1lem1div2  10288  faclbnd3  10704  abs3lemd  11191  xrbdtri  11265  modfsummod  11447  mertenslemi1  11524  sin01gt0  11750  cos01gt0  11751  sin02gt0  11752  dvds2subd  11815  dvds2addd  11817  dvdstrd  11818  zsupcllemex  11927  zssinfcl  11929  bezoutlemstep  11978  mulgcd  11997  gcddvdslcm  12053  lcmgcdeq  12063  mulgcddvds  12074  rpmulgcd2  12075  rpdvds  12079  divgcdcoprmex  12082  rpexp  12133  phimullem  12205  eulerthlem1  12207  eulerthlemrprm  12209  eulerthlemth  12212  prmdiveq  12216  pythagtriplem4  12248  pcqmul  12283  pcgcd1  12307  pcadd  12319  pockthlem  12334  exmidunben  12407  mulgass  12905  lmtopcnp  13414  blin2  13596  xmetxp  13671  tgqioo  13711  cncfmptid  13747  negcncf  13752  limcimolemlt  13797  sinq12gt0  13915  logdivlti  13966  2sqlem5  14119  2sqlem8  14123
  Copyright terms: Public domain W3C validator