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

Theorem mpdan 415
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
StepHypRef Expression
1 id 19 . 2  |-  ( ph  ->  ph )
2 mpdan.1 . 2  |-  ( ph  ->  ps )
3 mpdan.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
41, 2, 3syl2anc 406 1  |-  ( ph  ->  ch )
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-ia3 107
This theorem is referenced by:  mpidan  417  mpan2  419  mpjaodan  770  mpd3an3  1299  eueq2dc  2828  csbiegf  3011  difsnb  3631  reusv3i  4348  fvmpt3  5466  ffvelrnd  5522  fnressn  5572  fliftel1  5661  f1oiso2  5694  riota5f  5720  1stvalg  6006  2ndvalg  6007  brtpos2  6114  tfrlemibxssdm  6190  dom2lem  6632  php5  6718  nnfi  6732  xpfi  6784  supisoti  6863  ordiso2  6886  omp1eomlem  6945  onenon  7006  oncardval  7008  cardonle  7009  recidnq  7165  archnqq  7189  prarloclemarch2  7191  recexprlem1ssl  7405  recexprlem1ssu  7406  recexprlemss1l  7407  recexprlemss1u  7408  recexprlemex  7409  0idsr  7539  lep1  8560  suprlubex  8667  uz11  9297  xnegid  9582  eluzfz2  9752  fzsuc  9789  fzsuc2  9799  fzp1disj  9800  fzneuz  9821  fzp1nel  9824  exbtwnzlemex  9967  flhalf  10015  modqval  10037  frec2uzsucd  10114  frecuzrdgsuc  10127  uzsinds  10155  seq3p1  10175  seqp1cd  10179  expubnd  10290  iexpcyc  10337  binom2sub1  10346  hashennn  10466  shftfval  10533  shftcan1  10546  cjval  10557  reval  10561  imval  10562  cjmulrcl  10599  addcj  10603  absval  10713  resqrexlemdecn  10724  resqrexlemnmsq  10729  resqrexlemnm  10730  absneg  10762  abscj  10764  sqabsadd  10767  sqabssub  10768  ltabs  10799  dfabsmax  10929  negfi  10939  fsum3  11096  trirecip  11210  efval  11266  ege2le3  11276  efcan  11281  sinval  11308  cosval  11309  efi4p  11323  resin4p  11324  recos4p  11325  sincossq  11354  eirraplem  11379  iddvds  11402  1dvds  11403  bezoutlemstep  11581  coprmgcdb  11665  1idssfct  11692  exprmfct  11714  oddpwdclemdc  11746  phival  11784  setsn0fun  11891  cldval  12163  ntrfval  12164  clsfval  12165  neifval  12204  tx1cn  12333  ismet  12408  isxmet  12409  divcnap  12619  dvaddxxbr  12708  dvmulxxbr  12709  dvcoapbr  12714  bj-findis  12979
  Copyright terms: Public domain W3C validator