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

Step	Hyp	Ref	Expression
1		mp2and.2	. 2 |- ( ph -> ch )
2		mp2and.1	. . 3 |- ( ph -> ps )
3		mp2and.3	. . 3 |- ( ph -> ( ( ps /\ ch ) -> th ) )
4	2, 3	mpand 429	. 2 |- ( ph -> ( ch -> th ) )
5	1, 4	mpd 13	1 |- ( ph -> th )

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  4711  tfr0dm  6555  tfr1onlemaccex  6581  tfrcllemaccex  6594  ertrd  6785  th3qlem1  6873  en2prd  7061  findcard2  7148  findcard2s  7149  diffifi  7153  fimax2gtrilemstep  7160  fidcenumlemrk  7226  fidcenumlemr  7227  isbth  7239  nninfninc  7416  cc2lem  7585  ltbtwnnqq  7735  prarloclemarch2  7739  addlocprlemeqgt  7852  addnqprlemrl  7877  addnqprlemru  7878  mulnqprlemrl  7893  mulnqprlemru  7894  ltexprlemrl  7930  ltexprlemru  7932  addcanprleml  7934  addcanprlemu  7935  recexprlemloc  7951  recexprlem1ssu  7954  cauappcvgprlemladdfl  7975  caucvgprlemloc  7995  caucvgprprlemloccalc  8004  letrd  8402  lelttrd  8403  lttrd  8404  ltletrd  8702  le2addd  8842  le2subd  8843  ltleaddd  8844  leltaddd  8845  lt2subd  8847  ltmul12a  9139  lediv12a  9173  lemul12ad  9221  lemul12bd  9222  lt2halvesd  9491  uzind  9695  uztrn  9877  xrlttrd  10148  xrlelttrd  10149  xrltletrd  10150  xrletrd  10151  ixxss1  10243  ixxss2  10244  ixxss12  10245  zsupcllemex  10597  zssinfcl  10599  fldiv4p1lem1div2  10672  seqf1og  10890  faclbnd3  11113  abs3lemd  11894  xrbdtri  11969  modfsummod  12152  mertenslemi1  12229  sin01gt0  12456  cos01gt0  12457  sin02gt0  12458  dvds2subd  12521  dvds2addd  12523  dvdstrd  12524  bezoutlemstep  12701  mulgcd  12720  gcddvdslcm  12778  lcmgcdeq  12788  mulgcddvds  12799  rpmulgcd2  12800  rpdvds  12804  divgcdcoprmex  12807  rpexp  12858  phimullem  12930  eulerthlem1  12932  eulerthlemrprm  12934  eulerthlemth  12937  prmdiveq  12941  pythagtriplem4  12974  pcqmul  13009  pcgcd1  13034  pcadd  13046  pockthlem  13062  4sqlem16  13112  exmidunben  13198  mulgass  13897  lmtopcnp  15164  blin2  15346  xmetxp  15421  tgqioo  15469  cncfmptid  15511  negcncf  15519  limcimolemlt  15578  plyadd  15665  plymul  15666  sinq12gt0  15744  logdivlti  15795  mpodvdsmulf1o  15907  perfectlem1  15916  2sqlem5  16041  2sqlem8  16045