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

Theorem mp3an12 1222
 Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)
Hypotheses
Ref Expression
mp3an12.1
mp3an12.2
mp3an12.3
Assertion
Ref Expression
mp3an12

Proof of Theorem mp3an12
StepHypRef Expression
1 mp3an12.2 . 2
2 mp3an12.1 . . 3
3 mp3an12.3 . . 3
42, 3mp3an1 1219 . 2
51, 4mpan 400 1
 Colors of variables: wff set class Syntax hints:   wi 4   w3a 885 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 887 This theorem is referenced by:  ceqsralv  2585  brelrn  4567  funpr  4951  ener  6259  ltaddnq  6505  ltadd1sr  6861  mul02  7384  ltapi  7625  div0ap  7679  divclapzi  7723  divcanap1zi  7724  divcanap2zi  7725  divrecapzi  7726  divcanap3zi  7727  divcanap4zi  7728  divassapzi  7738  divmulapzi  7739  divdirapzi  7740  redivclapzi  7754  ltm1  7812  mulgt1  7829  recgt1i  7864  recreclt  7866  ltmul1i  7886  ltdiv1i  7887  ltmuldivi  7888  ltmul2i  7889  lemul1i  7890  lemul2i  7891  cju  7913  nnge1  7937  nngt0  7939  nnrecgt0  7951  elnnnn0c  8227  elnnz1  8268  recnz  8333  eluzsubi  8500  ge0gtmnf  8736  m1expcl2  9277  1exp  9284  expubnd  9311  expnbnd  9372  expnlbnd  9373  remim  9460  imval2  9494  cjdivapi  9535  absdivapzi  9750
 Copyright terms: Public domain W3C validator