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

Theorem mpdan 417
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 408 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  419  mpan2  421  mpjaodan  772  mpd3an3  1301  eueq2dc  2830  csbiegf  3013  difsnb  3633  reusv3i  4350  fvmpt3  5468  ffvelrnd  5524  fnressn  5574  fliftel1  5663  f1oiso2  5696  riota5f  5722  1stvalg  6008  2ndvalg  6009  brtpos2  6116  tfrlemibxssdm  6192  dom2lem  6634  php5  6720  nnfi  6734  xpfi  6786  supisoti  6865  ordiso2  6888  omp1eomlem  6947  onenon  7008  oncardval  7010  cardonle  7011  recidnq  7169  archnqq  7193  prarloclemarch2  7195  recexprlem1ssl  7409  recexprlem1ssu  7410  recexprlemss1l  7411  recexprlemss1u  7412  recexprlemex  7413  0idsr  7543  lep1  8571  suprlubex  8678  uz11  9316  xnegid  9610  eluzfz2  9780  fzsuc  9817  fzsuc2  9827  fzp1disj  9828  fzneuz  9849  fzp1nel  9852  exbtwnzlemex  9995  flhalf  10043  modqval  10065  frec2uzsucd  10142  frecuzrdgsuc  10155  uzsinds  10183  seq3p1  10203  seqp1cd  10207  expubnd  10318  iexpcyc  10365  binom2sub1  10374  hashennn  10494  shftfval  10561  shftcan1  10574  cjval  10585  reval  10589  imval  10590  cjmulrcl  10627  addcj  10631  absval  10741  resqrexlemdecn  10752  resqrexlemnmsq  10757  resqrexlemnm  10758  absneg  10790  abscj  10792  sqabsadd  10795  sqabssub  10796  ltabs  10827  dfabsmax  10957  negfi  10967  fsum3  11124  trirecip  11238  efval  11294  ege2le3  11304  efcan  11309  sinval  11336  cosval  11337  efi4p  11351  resin4p  11352  recos4p  11353  sincossq  11382  eirraplem  11410  iddvds  11433  1dvds  11434  bezoutlemstep  11612  coprmgcdb  11696  1idssfct  11723  exprmfct  11745  oddpwdclemdc  11778  phival  11816  setsn0fun  11923  cldval  12195  ntrfval  12196  clsfval  12197  neifval  12236  tx1cn  12365  ismet  12440  isxmet  12441  divcnap  12651  dvaddxxbr  12761  dvmulxxbr  12762  dvcoapbr  12767  bj-findis  13104
  Copyright terms: Public domain W3C validator