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

Theorem mp3an12 1306
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 1303 . 2  |-  ( ( ps  /\  ch )  ->  th )
51, 4mpan 421 1  |-  ( ch 
->  th )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  mp3an12i  1320  ceqsralv  2720  brelrn  4779  funpr  5182  fpm  6582  ener  6680  ltaddnq  7238  ltadd1sr  7607  map2psrprg  7636  mul02  8172  ltapi  8421  div0ap  8485  divclapzi  8530  divcanap1zi  8531  divcanap2zi  8532  divrecapzi  8533  divcanap3zi  8534  divcanap4zi  8535  divassapzi  8545  divmulapzi  8546  divdirapzi  8547  redivclapzi  8561  ltm1  8627  mulgt1  8644  recgt1i  8679  recreclt  8681  ltmul1i  8701  ltdiv1i  8702  ltmuldivi  8703  ltmul2i  8704  lemul1i  8705  lemul2i  8706  cju  8742  nnge1  8766  nngt0  8768  nnrecgt0  8781  elnnnn0c  9045  elnnz1  9100  recnz  9167  eluzsubi  9376  ge0gtmnf  9635  m1expcl2  10345  1exp  10352  m1expeven  10370  expubnd  10380  iexpcyc  10427  expnbnd  10445  expnlbnd  10446  remim  10663  imval2  10697  cjdivapi  10738  absdivapzi  10957  ef01bndlem  11497  sin01gt0  11502  cos01gt0  11503  cos12dec  11508  absefib  11511  efieq1re  11512  zeo3  11599  evend2  11620  cnbl0  12740  reeff1olem  12898  sincosq1sgn  12953  sincosq3sgn  12955  sincosq4sgn  12956  rpelogb  13072
  Copyright terms: Public domain W3C validator