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

Theorem mpdan 418
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 (𝜑𝜓)
mpdan.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpdan (𝜑𝜒)

Proof of Theorem mpdan
StepHypRef Expression
1 id 19 . 2 (𝜑𝜑)
2 mpdan.1 . 2 (𝜑𝜓)
3 mpdan.2 . 2 ((𝜑𝜓) → 𝜒)
41, 2, 3syl2anc 409 1 (𝜑𝜒)
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  420  mpan2  422  mpjaodan  788  mpd3an3  1317  eueq2dc  2860  csbiegf  3047  difsnb  3670  reusv3i  4387  fvmpt3  5507  ffvelrnd  5563  fnressn  5613  fliftel1  5702  f1oiso2  5735  riota5f  5761  1stvalg  6047  2ndvalg  6048  brtpos2  6155  tfrlemibxssdm  6231  dom2lem  6673  php5  6759  nnfi  6773  xpfi  6825  supisoti  6904  ordiso2  6927  omp1eomlem  6986  onenon  7056  oncardval  7058  cardonle  7059  recidnq  7224  archnqq  7248  prarloclemarch2  7250  recexprlem1ssl  7464  recexprlem1ssu  7465  recexprlemss1l  7466  recexprlemss1u  7467  recexprlemex  7468  0idsr  7598  lep1  8626  suprlubex  8733  uz11  9371  xnegid  9671  eluzfz2  9842  fzsuc  9879  fzsuc2  9889  fzp1disj  9890  fzneuz  9911  fzp1nel  9914  exbtwnzlemex  10057  flhalf  10105  modqval  10127  frec2uzsucd  10204  frecuzrdgsuc  10217  uzsinds  10245  seq3p1  10265  seqp1cd  10269  expubnd  10380  iexpcyc  10427  binom2sub1  10436  hashennn  10557  shftfval  10624  shftcan1  10637  cjval  10648  reval  10652  imval  10653  cjmulrcl  10690  addcj  10694  absval  10804  resqrexlemdecn  10815  resqrexlemnmsq  10820  resqrexlemnm  10821  absneg  10853  abscj  10855  sqabsadd  10858  sqabssub  10859  ltabs  10890  dfabsmax  11020  negfi  11030  fsum3  11187  trirecip  11301  efval  11402  ege2le3  11412  efcan  11417  sinval  11443  cosval  11444  efi4p  11458  resin4p  11459  recos4p  11460  sincossq  11489  eirraplem  11517  iddvds  11540  1dvds  11541  bezoutlemstep  11719  coprmgcdb  11803  1idssfct  11830  exprmfct  11852  oddpwdclemdc  11885  phival  11923  setsn0fun  12033  cldval  12305  ntrfval  12306  clsfval  12307  neifval  12346  tx1cn  12475  ismet  12550  isxmet  12551  divcnap  12761  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  bj-findis  13346
  Copyright terms: Public domain W3C validator