Theorem mpdan 421

Description: An inference based on modus ponens. (Contributed by NM, 23-May-1999.) (Proof shortened by Wolf Lammen, 22-Nov-2012.)

Hypotheses

Ref	Expression
mpdan.1	|- ( ph -> ps )
mpdan.2	|- ( ( ph /\ ps ) -> ch )

Assertion

Ref	Expression
mpdan	|- ( ph -> ch )

Proof of Theorem mpdan

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ph -> ph )
2		mpdan.1	. 2 |- ( ph -> ps )
3		mpdan.2	. 2 |- ( ( ph /\ ps ) -> ch )
4	1, 2, 3	syl2anc 411	1 |- ( ph -> ch )

Syntax hints:   -> wi 4   /\ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is referenced by:  mpidan  423  mpan2  425  mpjaodan  798  mpd3an3  1338  eueq2dc  2911  csbiegf  3101  difsnb  3736  reusv3i  4460  fvmpt3  5596  ffvelcdmd  5653  fnressn  5703  fliftel1  5795  f1oiso2  5828  riota5f  5855  1stvalg  6143  2ndvalg  6144  brtpos2  6252  tfrlemibxssdm  6328  dom2lem  6772  php5  6858  nnfi  6872  xpfi  6929  supisoti  7009  ordiso2  7034  omp1eomlem  7093  nnnninfeq2  7127  onenon  7183  oncardval  7185  cardonle  7186  recidnq  7392  archnqq  7416  prarloclemarch2  7418  recexprlem1ssl  7632  recexprlem1ssu  7633  recexprlemss1l  7634  recexprlemss1u  7635  recexprlemex  7636  0idsr  7766  lep1  8802  suprlubex  8909  uz11  9550  xnegid  9859  eluzfz2  10032  fzsuc  10069  fzsuc2  10079  fzp1disj  10080  fzneuz  10101  fzp1nel  10104  exbtwnzlemex  10250  flhalf  10302  modqval  10324  frec2uzsucd  10401  frecuzrdgsuc  10414  uzsinds  10442  seq3p1  10462  seqp1cd  10466  expubnd  10577  iexpcyc  10625  binom2sub1  10635  hashennn  10760  shftfval  10830  shftcan1  10843  cjval  10854  reval  10858  imval  10859  cjmulrcl  10896  addcj  10900  absval  11010  resqrexlemdecn  11021  resqrexlemnmsq  11026  resqrexlemnm  11027  absneg  11059  abscj  11061  sqabsadd  11064  sqabssub  11065  ltabs  11096  dfabsmax  11226  negfi  11236  fsum3  11395  trirecip  11509  fprodseq  11591  efval  11669  ege2le3  11679  efcan  11684  sinval  11710  cosval  11711  efi4p  11725  resin4p  11726  recos4p  11727  sincossq  11756  eirraplem  11784  iddvds  11811  1dvds  11812  bezoutlemstep  11998  coprmgcdb  12088  1idssfct  12115  exprmfct  12138  oddpwdclemdc  12173  phival  12213  odzphi  12246  oddprmdvds  12352  setsn0fun  12499  0subm  12871  grprcan  12910  isgrpid2  12913  grpinvid  12930  mulgval  12986  mulgnn0z  13010  0subg  13059  mgpplusgg  13134  mgpbasg  13136  mgpscag  13137  mgptsetg  13138  mgpdsg  13140  srgen1zr  13171  opprmulfvalg  13242  opprsllem  13246  1unit  13276  1rinv  13297  subrg1  13352  subrgmcl  13354  subrgdvds  13356  subrguss  13357  subrginv  13358  subrgdv  13359  subrgunit  13360  subrgugrp  13361  lmodfopne  13416  cnfldneg  13470  cldval  13602  ntrfval  13603  clsfval  13604  neifval  13643  tx1cn  13772  ismet  13847  isxmet  13848  divcnap  14058  dvaddxxbr  14168  dvmulxxbr  14169  dvcoapbr  14174  1lgs  14447  lgs1  14448  bj-charfun  14562  bj-findis  14734