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

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 (𝜑𝜓)
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 411 1 (𝜑𝜒)
Colors of variables: wff set class
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  3734  reusv3i  4455  fvmpt3  5590  ffvelcdmd  5647  fnressn  5697  fliftel1  5788  f1oiso2  5821  riota5f  5848  1stvalg  6136  2ndvalg  6137  brtpos2  6245  tfrlemibxssdm  6321  dom2lem  6765  php5  6851  nnfi  6865  xpfi  6922  supisoti  7002  ordiso2  7027  omp1eomlem  7086  nnnninfeq2  7120  onenon  7176  oncardval  7178  cardonle  7179  recidnq  7370  archnqq  7394  prarloclemarch2  7396  recexprlem1ssl  7610  recexprlem1ssu  7611  recexprlemss1l  7612  recexprlemss1u  7613  recexprlemex  7614  0idsr  7744  lep1  8778  suprlubex  8885  uz11  9526  xnegid  9833  eluzfz2  10005  fzsuc  10042  fzsuc2  10052  fzp1disj  10053  fzneuz  10074  fzp1nel  10077  exbtwnzlemex  10223  flhalf  10275  modqval  10297  frec2uzsucd  10374  frecuzrdgsuc  10387  uzsinds  10415  seq3p1  10435  seqp1cd  10439  expubnd  10550  iexpcyc  10597  binom2sub1  10607  hashennn  10731  shftfval  10801  shftcan1  10814  cjval  10825  reval  10829  imval  10830  cjmulrcl  10867  addcj  10871  absval  10981  resqrexlemdecn  10992  resqrexlemnmsq  10997  resqrexlemnm  10998  absneg  11030  abscj  11032  sqabsadd  11035  sqabssub  11036  ltabs  11067  dfabsmax  11197  negfi  11207  fsum3  11366  trirecip  11480  fprodseq  11562  efval  11640  ege2le3  11650  efcan  11655  sinval  11681  cosval  11682  efi4p  11696  resin4p  11697  recos4p  11698  sincossq  11727  eirraplem  11755  iddvds  11782  1dvds  11783  bezoutlemstep  11968  coprmgcdb  12058  1idssfct  12085  exprmfct  12108  oddpwdclemdc  12143  phival  12183  odzphi  12216  oddprmdvds  12322  setsn0fun  12469  0subm  12748  grprcan  12787  isgrpid2  12790  grpinvid  12807  mulgval  12862  mulgnn0z  12885  mgpplusgg  12948  mgpbasg  12950  mgpscag  12951  mgptsetg  12952  mgpdsg  12954  srgen1zr  12984  opprmulfvalg  13054  opprsllem  13058  1unit  13088  1rinv  13109  cldval  13232  ntrfval  13233  clsfval  13234  neifval  13273  tx1cn  13402  ismet  13477  isxmet  13478  divcnap  13688  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  1lgs  14077  lgs1  14078  bj-charfun  14181  bj-findis  14353
  Copyright terms: Public domain W3C validator