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

Theorem mpdan 406
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 397 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mpan2  409  mpjaodan  720  mpd3an3  1242  eueq2dc  2734  csbiegf  2915  difsnb  3531  reusv3i  4216  fvmpt3  5276  ffvelrnd  5328  fnressn  5374  fliftel1  5459  f1oiso2  5491  riota5f  5517  1stvalg  5794  2ndvalg  5795  brtpos2  5894  tfrlemibxssdm  5969  dom2lem  6280  php5  6349  nnfi  6361  ordiso2  6385  onenon  6392  oncardval  6394  cardonle  6395  recidnq  6519  archnqq  6543  prarloclemarch2  6545  recexprlem1ssl  6759  recexprlem1ssu  6760  recexprlemss1l  6761  recexprlemss1u  6762  recexprlemex  6763  0idsr  6880  lep1  7856  uz11  8561  eluzfz2  8968  fzsuc  9003  fzsuc2  9013  fzp1disj  9014  fzneuz  9035  fzp1nel  9038  flhalf  9217  modqval  9239  frecuzrdgsuc  9330  iseqcl  9352  iseqp1  9354  expubnd  9442  shftfval  9614  shftcan1  9627  cjval  9637  reval  9641  imval  9642  cjmulrcl  9679  addcj  9683  absval  9791  resqrexlemdecn  9802  resqrexlemnmsq  9807  resqrexlemnm  9808  absneg  9840  abscj  9842  sqabsadd  9845  sqabssub  9846  ltabs  9877  iddvds  10084  1dvds  10085  oddpwdclemdc  10204  bj-findis  10434
  Copyright terms: Public domain W3C validator