Theorem mp2and 437

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 433	. 2 |- ( ph -> ( ch -> th ) )
5	1, 4	mpd 13	1 |- ( ph -> th )

This proof depends on syntax axioms:   -> wi 4   /\ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  tfisi  4734  tfr0dm  6593  tfr1onlemaccex  6619  tfrcllemaccex  6632  ertrd  6823  th3qlem1  6911  en2prd  7106  findcard2  7193  findcard2s  7194  diffifi  7198  fimax2gtrilemstep  7205  fidcenumlemrk  7271  fidcenumlemr  7272  isbth  7284  nninfninc  7464  cc2lem  7633  ltbtwnnqq  7783  prarloclemarch2  7787  addlocprlemeqgt  7900  addnqprlemrl  7925  addnqprlemru  7926  mulnqprlemrl  7941  mulnqprlemru  7942  ltexprlemrl  7978  ltexprlemru  7980  addcanprleml  7982  addcanprlemu  7983  recexprlemloc  7999  recexprlem1ssu  8002  cauappcvgprlemladdfl  8023  caucvgprlemloc  8043  caucvgprprlemloccalc  8052  letrd  8452  lelttrd  8453  lttrd  8454  ltletrd  8753  le2addd  8894  le2subd  8895  ltleaddd  8896  leltaddd  8897  lt2subd  8899  ltmul12a  9193  lediv12a  9227  lemul12ad  9275  lemul12bd  9276  lt2halvesd  9558  uzind  9762  uztrn  9949  xrlttrd  10222  xrlelttrd  10223  xrltletrd  10224  xrletrd  10225  ixxss1  10317  ixxss2  10318  ixxss12  10319  zsupcllemex  10674  zssinfcl  10676  fldiv4p1lem1div2  10755  seqf1og  10973  faclbnd3  11197  abs3lemd  11984  xrbdtri  12061  modfsummod  12244  mertenslemi1  12321  sin01gt0  12548  cos01gt0  12549  sin02gt0  12550  dvds2subd  12613  dvds2addd  12615  dvdstrd  12616  bezoutlemstep  12793  mulgcd  12812  gcddvdslcm  12870  lcmgcdeq  12880  mulgcddvds  12891  rpmulgcd2  12892  rpdvds  12896  divgcdcoprmex  12899  rpexp  12951  phimullem  13026  eulerthlem1  13028  eulerthlemrprm  13030  eulerthlemth  13033  prmdiveq  13037  pythagtriplem4  13070  pcqmul  13105  pcgcd1  13130  pcadd  13142  pockthlem  13158  4sqlem16  13208  exmidunben  13369  mulgass  14015  lmtopcnp  15442  blin2  15624  xmetxp  15699  tgqioo  15747  cncfmptid  15789  negcncf  15797  limcimolemlt  15856  plyadd  15943  plymul  15944  sinq12gt0  16023  logdivlti  16077  ppiprm  16225  mpodvdsmulf1o  16250  perfectlem1  16265  2sqlem5  16409  2sqlem8  16413