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

Theorem mp3an12 1261
Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1  |-  ph
mp3an12.2  |-  ps
mp3an12.3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
Assertion
Ref Expression
mp3an12  |-  ( ch 
->  th )

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2  |-  ps
2 mp3an12.1 . . 3  |-  ph
3 mp3an12.3 . . 3  |-  ( (
ph  /\  ps  /\  ch )  ->  th )
42, 3mp3an1 1258 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 415 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  mp3an12i  1275  ceqsralv  2644  brelrn  4638  funpr  5033  fpm  6392  ener  6450  ltaddnq  6913  ltadd1sr  7269  mul02  7812  ltapi  8055  div0ap  8111  divclapzi  8156  divcanap1zi  8157  divcanap2zi  8158  divrecapzi  8159  divcanap3zi  8160  divcanap4zi  8161  divassapzi  8171  divmulapzi  8172  divdirapzi  8173  redivclapzi  8187  ltm1  8245  mulgt1  8262  recgt1i  8297  recreclt  8299  ltmul1i  8319  ltdiv1i  8320  ltmuldivi  8321  ltmul2i  8322  lemul1i  8323  lemul2i  8324  cju  8359  nnge1  8383  nngt0  8385  nnrecgt0  8397  elnnnn0c  8654  elnnz1  8709  recnz  8775  eluzsubi  8981  ge0gtmnf  9220  m1expcl2  9879  1exp  9886  m1expeven  9904  expubnd  9914  iexpcyc  9960  expnbnd  9977  expnlbnd  9978  remim  10193  imval2  10227  cjdivapi  10268  absdivapzi  10486  zeo3  10774  evend2  10795
  Copyright terms: Public domain W3C validator