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

Theorem mpan2 416
Description: An inference based on modus ponens. (Contributed by NM, 16-Sep-1993.) (Proof shortened by Wolf Lammen, 19-Nov-2012.)
Hypotheses
Ref Expression
mpan2.1  |-  ps
mpan2.2  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mpan2  |-  ( ph  ->  ch )

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3  |-  ps
21a1i 9 . 2  |-  ( ph  ->  ps )
3 mpan2.2 . 2  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpdan 412 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:  mpanr12  430  mp3an23  1263  equs4  1657  sb4bor  1760  eueq2dc  2779  sbcgf  2895  csbconstgf  2933  sbcnestg  2970  csbnestg  2971  csbnest1g  2972  ssindif0im  3330  mpteq1  3896  iinexgm  3963  mss  4025  eusv2nf  4250  eldifpw  4270  ordtriexmid  4309  onsucsssucexmid  4314  ordsucunielexmid  4318  nn0suc  4390  xpss1  4514  xpiindim  4539  reldm0  4620  elrnmpt1s  4651  resdm  4716  resid  4731  eliniseg  4765  trinxp  4788  inimasn  4811  ssrnres  4835  cnveq0  4849  coi2  4909  relrelss  4919  funcnvres  5048  funimaex  5060  fnresin1  5089  fnresin2  5090  fresin  5145  dffv3g  5257  ssimaex  5321  dmfco  5328  fvmpt  5337  fsn  5425  fsn2  5427  elabrex  5491  f1elima  5506  2ndconst  5937  tposfun  5972  tpostpos2  5977  tfrexlem  6046  tfri3  6079  rdgruledefgg  6087  rdgss  6095  frecsuclem  6118  frecrdg  6120  oa0  6165  om0  6166  oei0  6167  oav2  6171  oa1suc  6175  nnmsucr  6196  nnm1  6228  nnm2  6229  ecelqsg  6290  ecidg  6301  xpiderm  6308  qsel  6314  mapdm0  6365  map0e  6388  mapsnconst  6396  map1  6474  xp1en  6484  xpcomco  6487  xpmapenlem  6510  findcard2s  6551  findcard2d  6552  findcard2sd  6553  exmidpw  6569  sbthlem7  6608  eqinfti  6651  djueq1  6669  finomni  6732  pm54.43  6754  mulidpi  6813  nlt1pig  6836  indpi  6837  halfnqq  6905  archnqq  6912  prarloclemarch  6913  prarloclemarch2  6914  nnnq  6917  nq0a0  6952  addpinq1  6959  prarloclemlt  6988  prarloclemlo  6989  prarloclem3  6992  prarloclemcalc  6997  nqprm  7037  addnqpr1  7057  1idprl  7085  1idpru  7086  1idpr  7087  recexprlem1ssl  7128  recexprlem1ssu  7129  ltmprr  7137  0idsr  7249  1idsr  7250  00sr  7251  pn0sr  7253  negexsr  7254  recexgt0sr  7255  archsr  7263  prsrcl  7265  prsradd  7267  elrealeu  7303  pitonnlem1p1  7319  peano2nnnn  7326  ax1rid  7348  axcnre  7352  peano5nnnn  7363  peano2cn  7553  peano2re  7554  addid2  7557  subid  7637  subid1  7638  negid  7665  negeq0  7672  peano2cnm  7684  peano2rem  7685  mul01  7803  lt0neg1  7882  le0neg1  7884  recexre  7988  inelr  7994  rimul  7995  reapmul1  8005  apsqgt0  8011  mulge0  8029  negap0  8039  divvalap  8072  rerecclap  8128  div2negap  8133  divgt0i2i  8305  peano5nni  8352  nnge1  8372  times2  8471  addltmul  8577  nn0p1nn  8637  peano2nn0  8638  nn0lele2xi  8649  znnnlt1  8723  nn0lt10b  8752  prime  8770  msqznn  8771  zeo  8776  elnn1uz2  9018  qreccl  9051  qdivcl  9052  irrmul  9056  rphalfcl  9085  rpnegap  9090  ltpnf  9175  nltmnf  9182  pnfge  9183  xlt0neg1  9224  xle0neg1  9226  elioopnf  9309  elicopnf  9311  iccshftri  9336  iccshftli  9338  iccdili  9340  icccntri  9342  fzprval  9418  fzofzp1  9558  fzostep1  9568  flqge0nn0  9620  flqge1nn  9621  fldiv4p1lem1div2  9632  expivallem  9846  expival  9847  exp1  9851  qexpclz  9866  nn0sqcl  9872  expeq0  9876  expubnd  9902  sqval  9903  sqeq0  9908  resqcl  9912  zsqcl  9915  iexpcyc  9948  binom21  9955  bcnn  10053  bcn2  10060  bcn2p1  10066  bcnm1  10068  fihasheq0  10090  hashsng  10094  fihashen1  10095  fimaxq  10123  shftfibg  10142  shftfib  10145  reim0  10182  imval2  10215  cjap0  10228  cjne0  10229  rexuz3  10310  resqrexlemover  10330  abs00  10384  abssq  10401  nn0abscl  10405  nnabscl  10420  abs2dif  10426  max0addsup  10539  climshft  10577  dvdsval2  10665  zdvdsdc  10683  dvdsmul2  10685  dvdsmulcr  10692  dvdsabseq  10714  divconjdvds  10716  alzdvds  10721  fzo0dvdseq  10724  odd2np1lem  10738  mod2eq1n2dvds  10745  flodddiv4  10800  flodddiv4t2lthalf  10803  gcdmndc  10806  gcd0id  10836  gcd1  10844  dfgcd2  10869  gcdmultiple  10875  gcdmultiplez  10876  dvdssq  10886  lcmmndc  10910  lcm0val  10913  dvdslcm  10917  lcmeq0  10919  lcmgcd  10926  lcmdvds  10927  lcmid  10928  lcm1  10929  cncongr2  10952  isprm3  10966  prm2orodd  10974  sqrt2irrap  11024  phiprm  11065  unennn  11076  bj-inf2vnlem1  11294  nninfsellemeqinf  11337
  Copyright terms: Public domain W3C validator