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

Theorem mp2and 424
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 420 . 2  |-  ( ph  ->  ( ch  ->  th )
)
51, 4mpd 13 1  |-  ( ph  ->  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:  tfisi  4330  tfr0dm  5965  tfr1onlemaccex  5991  tfrcllemaccex  6004  ertrd  6181  th3qlem1  6267  findcard2  6413  findcard2s  6414  diffifi  6418  ltbtwnnqq  6656  prarloclemarch2  6660  addlocprlemeqgt  6773  addnqprlemrl  6798  addnqprlemru  6799  mulnqprlemrl  6814  mulnqprlemru  6815  ltexprlemrl  6851  ltexprlemru  6853  addcanprleml  6855  addcanprlemu  6856  recexprlemloc  6872  recexprlem1ssu  6875  cauappcvgprlemladdfl  6896  caucvgprlemloc  6916  caucvgprprlemloccalc  6925  letrd  7289  lelttrd  7290  lttrd  7291  ltletrd  7583  le2addd  7719  le2subd  7720  ltleaddd  7721  leltaddd  7722  lt2subd  7724  ltmul12a  7994  lediv12a  8028  lemul12ad  8076  lemul12bd  8077  lt2halvesd  8334  uzind  8528  uztrn  8705  xrlttrd  8944  xrlelttrd  8945  xrltletrd  8946  xrletrd  8947  ixxss1  8992  ixxss2  8993  ixxss12  8994  fldiv4p1lem1div2  9376  faclbnd3  9756  abs3lemd  10214  dvds2subd  10365  zsupcllemex  10475  zssinfcl  10477  bezoutlemstep  10519  mulgcd  10538  gcddvdslcm  10588  lcmgcdeq  10598  mulgcddvds  10609  rpmulgcd2  10610  rpdvds  10614  divgcdcoprmex  10617  rpexp  10665
  Copyright terms: Public domain W3C validator