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  2910  csbiegf  3100  difsnb  3735  reusv3i  4458  fvmpt3  5594  ffvelcdmd  5651  fnressn  5701  fliftel1  5792  f1oiso2  5825  riota5f  5852  1stvalg  6140  2ndvalg  6141  brtpos2  6249  tfrlemibxssdm  6325  dom2lem  6769  php5  6855  nnfi  6869  xpfi  6926  supisoti  7006  ordiso2  7031  omp1eomlem  7090  nnnninfeq2  7124  onenon  7180  oncardval  7182  cardonle  7183  recidnq  7389  archnqq  7413  prarloclemarch2  7415  recexprlem1ssl  7629  recexprlem1ssu  7630  recexprlemss1l  7631  recexprlemss1u  7632  recexprlemex  7633  0idsr  7763  lep1  8798  suprlubex  8905  uz11  9546  xnegid  9855  eluzfz2  10027  fzsuc  10064  fzsuc2  10074  fzp1disj  10075  fzneuz  10096  fzp1nel  10099  exbtwnzlemex  10245  flhalf  10297  modqval  10319  frec2uzsucd  10396  frecuzrdgsuc  10409  uzsinds  10437  seq3p1  10457  seqp1cd  10461  expubnd  10572  iexpcyc  10619  binom2sub1  10629  hashennn  10753  shftfval  10823  shftcan1  10836  cjval  10847  reval  10851  imval  10852  cjmulrcl  10889  addcj  10893  absval  11003  resqrexlemdecn  11014  resqrexlemnmsq  11019  resqrexlemnm  11020  absneg  11052  abscj  11054  sqabsadd  11057  sqabssub  11058  ltabs  11089  dfabsmax  11219  negfi  11229  fsum3  11388  trirecip  11502  fprodseq  11584  efval  11662  ege2le3  11672  efcan  11677  sinval  11703  cosval  11704  efi4p  11718  resin4p  11719  recos4p  11720  sincossq  11749  eirraplem  11777  iddvds  11804  1dvds  11805  bezoutlemstep  11990  coprmgcdb  12080  1idssfct  12107  exprmfct  12130  oddpwdclemdc  12165  phival  12205  odzphi  12238  oddprmdvds  12344  setsn0fun  12491  0subm  12803  grprcan  12842  isgrpid2  12845  grpinvid  12862  mulgval  12918  mulgnn0z  12941  0subg  12990  mgpplusgg  13065  mgpbasg  13067  mgpscag  13068  mgptsetg  13069  mgpdsg  13071  srgen1zr  13102  opprmulfvalg  13173  opprsllem  13177  1unit  13207  1rinv  13228  subrg1  13290  subrgmcl  13292  subrgdvds  13294  subrguss  13295  subrginv  13296  subrgdv  13297  subrgunit  13298  subrgugrp  13299  cnfldneg  13336  cldval  13470  ntrfval  13471  clsfval  13472  neifval  13511  tx1cn  13640  ismet  13715  isxmet  13716  divcnap  13926  dvaddxxbr  14036  dvmulxxbr  14037  dvcoapbr  14042  1lgs  14315  lgs1  14316  bj-charfun  14419  bj-findis  14591