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

Theorem mpdan 412
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 403 1  |-  ( ph  ->  ch )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106
This theorem is referenced by:  mpidan  414  mpan2  416  mpjaodan  745  mpd3an3  1270  eueq2dc  2766  csbiegf  2947  difsnb  3536  reusv3i  4217  fvmpt3  5283  ffvelrnd  5335  fnressn  5381  fliftel1  5465  f1oiso2  5497  riota5f  5523  1stvalg  5800  2ndvalg  5801  brtpos2  5900  tfrlemibxssdm  5976  dom2lem  6319  php5  6393  nnfi  6407  supisoti  6482  ordiso2  6505  onenon  6512  oncardval  6514  cardonle  6515  recidnq  6645  archnqq  6669  prarloclemarch2  6671  recexprlem1ssl  6885  recexprlem1ssu  6886  recexprlemss1l  6887  recexprlemss1u  6888  recexprlemex  6889  0idsr  7006  lep1  7990  suprlubex  8097  uz11  8722  eluzfz2  9127  fzsuc  9162  fzsuc2  9172  fzp1disj  9173  fzneuz  9194  fzp1nel  9197  exbtwnzlemex  9336  flhalf  9384  modqval  9406  frec2uzsucd  9483  frecuzrdgsuc  9496  uzsinds  9518  iseqp1  9538  iseqp1t  9539  expubnd  9630  iexpcyc  9676  sizeennn  9804  shftfval  9847  shftcan1  9860  cjval  9870  reval  9874  imval  9875  cjmulrcl  9912  addcj  9916  absval  10025  resqrexlemdecn  10036  resqrexlemnmsq  10041  resqrexlemnm  10042  absneg  10074  abscj  10076  sqabsadd  10079  sqabssub  10080  ltabs  10111  dfabsmax  10241  negfi  10248  iddvds  10353  1dvds  10354  bezoutlemstep  10530  coprmgcdb  10614  1idssfct  10641  exprmfct  10663  oddpwdclemdc  10695  bj-findis  10932
  Copyright terms: Public domain W3C validator