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  1261  equs4  1654  sb4bor  1757  eueq2dc  2766  sbcgf  2882  csbconstgf  2920  sbcnestg  2956  csbnestg  2957  csbnest1g  2958  ssindif0im  3310  mpteq1  3870  iinexgm  3937  mss  3989  eusv2nf  4214  eldifpw  4234  ordtriexmid  4273  onsucsssucexmid  4278  ordsucunielexmid  4282  nn0suc  4353  xpss1  4476  xpiindim  4501  reldm0  4581  elrnmpt1s  4612  resdm  4677  resid  4692  eliniseg  4725  trinxp  4748  inimasn  4771  ssrnres  4793  cnveq0  4807  coi2  4867  relrelss  4874  funcnvres  5003  funimaex  5015  fnresin1  5044  fnresin2  5045  fresin  5099  dffv3g  5205  ssimaex  5266  dmfco  5273  fvmpt  5281  fsn  5367  fsn2  5369  elabrex  5429  f1elima  5444  2ndconst  5874  tposfun  5909  tpostpos2  5914  tfrexlem  5983  tfri3  6016  rdgruledefgg  6024  rdgss  6032  frecsuclem  6055  frecrdg  6057  oa0  6101  om0  6102  oei0  6103  oav2  6107  oa1suc  6111  nnmsucr  6132  nnm1  6163  nnm2  6164  ecelqsg  6225  ecidg  6236  xpiderm  6243  qsel  6249  xp1en  6367  xpcomco  6370  findcard2s  6424  findcard2d  6425  findcard2sd  6426  eqinfti  6492  pm54.43  6518  mulidpi  6570  nlt1pig  6593  indpi  6594  halfnqq  6662  archnqq  6669  prarloclemarch  6670  prarloclemarch2  6671  nnnq  6674  nq0a0  6709  addpinq1  6716  prarloclemlt  6745  prarloclemlo  6746  prarloclem3  6749  prarloclemcalc  6754  nqprm  6794  addnqpr1  6814  1idprl  6842  1idpru  6843  1idpr  6844  recexprlem1ssl  6885  recexprlem1ssu  6886  ltmprr  6894  0idsr  7006  1idsr  7007  00sr  7008  pn0sr  7010  negexsr  7011  recexgt0sr  7012  archsr  7020  prsrcl  7022  prsradd  7024  elrealeu  7060  pitonnlem1p1  7076  peano2nnnn  7083  ax1rid  7105  axcnre  7109  peano5nnnn  7120  peano2cn  7310  peano2re  7311  addid2  7314  subid  7394  subid1  7395  negid  7422  negeq0  7429  peano2cnm  7441  peano2rem  7442  mul01  7560  lt0neg1  7639  le0neg1  7641  recexre  7745  inelr  7751  rimul  7752  reapmul1  7762  apsqgt0  7768  mulge0  7786  negap0  7796  divvalap  7829  rerecclap  7885  div2negap  7890  divgt0i2i  8062  peano5nni  8109  nnge1  8129  times2  8228  addltmul  8334  nn0p1nn  8394  peano2nn0  8395  nn0lele2xi  8406  znnnlt1  8480  nn0lt10b  8509  prime  8527  msqznn  8528  zeo  8533  elnn1uz2  8775  qreccl  8808  qdivcl  8809  irrmul  8813  rphalfcl  8842  rpnegap  8847  ltpnf  8932  nltmnf  8939  pnfge  8940  xlt0neg1  8981  xle0neg1  8983  elioopnf  9066  elicopnf  9068  iccshftri  9093  iccshftli  9095  iccdili  9097  icccntri  9099  fzprval  9175  fzofzp1  9313  fzostep1  9323  flqge0nn0  9375  flqge1nn  9376  fldiv4p1lem1div2  9387  expivallem  9574  expival  9575  exp1  9579  qexpclz  9594  nn0sqcl  9600  expeq0  9604  expubnd  9630  sqval  9631  sqeq0  9636  resqcl  9640  zsqcl  9643  iexpcyc  9676  binom21  9683  bcnn  9781  bcn2  9788  bcn2p1  9794  bcnm1  9796  sizeeq0  9818  sizesng  9822  sizeen1  9823  shftfibg  9846  shftfib  9849  reim0  9886  imval2  9919  cjap0  9932  cjne0  9933  rexuz3  10014  resqrexlemover  10034  abs00  10088  abssq  10105  nn0abscl  10109  nnabscl  10124  abs2dif  10130  max0addsup  10243  climshft  10281  dvdsval2  10343  zdvdsdc  10361  dvdsmul2  10363  dvdsmulcr  10370  dvdsabseq  10392  divconjdvds  10394  alzdvds  10399  fzo0dvdseq  10402  odd2np1lem  10416  mod2eq1n2dvds  10423  flodddiv4  10478  flodddiv4t2lthalf  10481  gcdmndc  10484  gcd0id  10514  gcd1  10522  dfgcd2  10547  gcdmultiple  10553  gcdmultiplez  10554  dvdssq  10564  lcmmndc  10588  lcm0val  10591  dvdslcm  10595  lcmeq0  10597  lcmgcd  10604  lcmdvds  10605  lcmid  10606  lcm1  10607  cncongr2  10630  isprm3  10644  prm2orodd  10652  sqrt2irrap  10702  unennn  10708  bj-inf2vnlem1  10923
  Copyright terms: Public domain W3C validator