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

Theorem mp2and 427
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 423 . 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  4469  tfr0dm  6185  tfr1onlemaccex  6211  tfrcllemaccex  6224  ertrd  6411  th3qlem1  6497  findcard2  6749  findcard2s  6750  diffifi  6754  fimax2gtrilemstep  6760  fidcenumlemrk  6808  fidcenumlemr  6809  isbth  6821  ltbtwnnqq  7187  prarloclemarch2  7191  addlocprlemeqgt  7304  addnqprlemrl  7329  addnqprlemru  7330  mulnqprlemrl  7345  mulnqprlemru  7346  ltexprlemrl  7382  ltexprlemru  7384  addcanprleml  7386  addcanprlemu  7387  recexprlemloc  7403  recexprlem1ssu  7406  cauappcvgprlemladdfl  7427  caucvgprlemloc  7447  caucvgprprlemloccalc  7456  letrd  7850  lelttrd  7851  lttrd  7852  ltletrd  8149  le2addd  8288  le2subd  8289  ltleaddd  8290  leltaddd  8291  lt2subd  8293  ltmul12a  8575  lediv12a  8609  lemul12ad  8657  lemul12bd  8658  lt2halvesd  8918  uzind  9113  uztrn  9291  xrlttrd  9532  xrlelttrd  9533  xrltletrd  9534  xrletrd  9535  ixxss1  9627  ixxss2  9628  ixxss12  9629  fldiv4p1lem1div2  10018  faclbnd3  10429  abs3lemd  10913  xrbdtri  10985  modfsummod  11167  mertenslemi1  11244  sin01gt0  11367  cos01gt0  11368  sin02gt0  11369  dvds2subd  11425  zsupcllemex  11535  zssinfcl  11537  bezoutlemstep  11581  mulgcd  11600  gcddvdslcm  11650  lcmgcdeq  11660  mulgcddvds  11671  rpmulgcd2  11672  rpdvds  11676  divgcdcoprmex  11679  rpexp  11727  phimullem  11796  exmidunben  11834  lmtopcnp  12314  blin2  12496  xmetxp  12571  tgqioo  12611  cncfmptid  12647  negcncf  12652  limcimolemlt  12676
  Copyright terms: Public domain W3C validator