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

Theorem mpan2 425
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 𝜓
mpan2.2 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mpan2 (𝜑𝜒)

Proof of Theorem mpan2
StepHypRef Expression
1 mpan2.1 . . 3 𝜓
21a1i 9 . 2 (𝜑𝜓)
3 mpan2.2 . 2 ((𝜑𝜓) → 𝜒)
42, 3mpdan 421 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108
This theorem is referenced by:  mpanr12  439  mp3an23  1329  equs4  1725  sb4bor  1835  elvd  2742  eueq2dc  2910  sbcgf  3030  csbconstgf  3070  sbcnestg  3110  csbnestg  3111  csbnest1g  3112  ssindif0im  3482  mpteq1  4084  iinexgm  4151  mss  4222  eusv2nf  4452  eldifpw  4473  ordtriexmid  4516  onsucsssucexmid  4522  ordsucunielexmid  4526  nn0suc  4599  xpss1  4732  xpiindim  4759  reldm0  4840  elrnmpt1s  4872  resdm  4941  resid  4959  eliniseg  4993  trinxp  5017  inimasn  5041  ssrnres  5066  cnveq0  5080  coi2  5140  relrelss  5150  funcnvres  5284  funimaex  5296  fnresin1  5325  fnresin2  5326  fresin  5389  dffv3g  5506  ssimaex  5572  dmfco  5579  fvmpt  5588  fsn  5683  fsn2  5685  elabrex  5752  f1elima  5767  2ndconst  6216  tposfun  6254  tpostpos2  6259  tfrexlem  6328  tfri3  6361  rdgruledefgg  6369  rdgss  6377  frecsuclem  6400  frecrdg  6402  oa0  6451  om0  6452  oei0  6453  oav2  6457  oa1suc  6461  nnmsucr  6482  nnm1  6519  nnm2  6520  ecelqsg  6581  ecidg  6592  xpider  6599  qsel  6605  mapdm0  6656  map0e  6679  mapsnconst  6687  ixpsnf1o  6729  map1  6805  xp1en  6816  xpcomco  6819  xpmapenlem  6842  findcard2s  6883  findcard2d  6884  findcard2sd  6885  exmidpw  6901  fidcenumlemr  6947  sbthlem7  6955  eqinfti  7012  djueq1  7032  omp1eomlem  7086  endjusym  7088  eninl  7089  eninr  7090  difinfsn  7092  finomni  7131  pm54.43  7182  exmidonfinlem  7185  mulidpi  7295  nlt1pig  7318  indpi  7319  halfnqq  7387  archnqq  7394  prarloclemarch  7395  prarloclemarch2  7396  nnnq  7399  nq0a0  7434  addpinq1  7441  prarloclemlt  7470  prarloclemlo  7471  prarloclem3  7474  prarloclemcalc  7479  nqprm  7519  addnqpr1  7539  1idprl  7567  1idpru  7568  1idpr  7569  recexprlem1ssl  7610  recexprlem1ssu  7611  ltmprr  7619  0idsr  7744  1idsr  7745  00sr  7746  pn0sr  7748  negexsr  7749  recexgt0sr  7750  ltm1sr  7754  archsr  7759  prsrcl  7761  prsradd  7763  mappsrprg  7781  map2psrprg  7782  elrealeu  7806  pitonnlem1p1  7823  peano2nnnn  7830  ax1rid  7854  axcnre  7858  peano5nnnn  7869  peano2cn  8069  peano2re  8070  addid2  8073  subid  8153  subid1  8154  negid  8181  negeq0  8188  peano2cnm  8200  peano2rem  8201  mul01  8323  lt0neg1  8402  le0neg1  8404  recexre  8512  inelr  8518  rimul  8519  reapmul1  8529  apsqgt0  8535  mulge0  8553  negap0  8564  divvalap  8607  rerecclap  8663  div2negap  8668  divgt0i2i  8850  peano5nni  8898  nnge1  8918  times2  9024  addltmul  9131  nn0p1nn  9191  peano2nn0  9192  nn0lele2xi  9203  znnnlt1  9277  nn0lt10b  9309  prime  9328  msqznn  9329  zeo  9334  elnn1uz2  9583  qreccl  9618  qdivcl  9619  irrmul  9623  rphalfcl  9655  rpnegap  9660  zgt1rpn0n1  9669  ltpnf  9754  nltmnf  9762  pnfge  9763  xlt0neg1  9812  xle0neg1  9814  xaddpnf1  9820  xaddmnf1  9822  xaddid1  9836  xsubge0  9855  xleaddadd  9861  elioopnf  9941  elicopnf  9943  iccshftri  9969  iccshftli  9971  iccdili  9973  icccntri  9975  fzprval  10055  fzofzp1  10200  fzostep1  10210  flqge0nn0  10266  flqge1nn  10267  fldiv4p1lem1div2  10278  exp1  10499  qexpclz  10514  nn0sqcl  10520  expeq0  10524  expubnd  10550  sqval  10551  sqeq0  10556  resqcl  10560  zsqcl  10563  iexpcyc  10597  binom21  10605  bcnn  10708  bcn2  10715  bcn2p1  10721  bcnm1  10723  fihasheq0  10744  hashsng  10749  fihashen1  10750  fimaxq  10778  shftfibg  10800  shftfib  10803  reim0  10841  imval2  10874  cjap0  10887  cjne0  10888  rexuz3  10970  resqrexlemover  10990  abssq  11061  nn0abscl  11065  nnabscl  11080  abs2dif  11086  max0addsup  11199  climshft  11283  bcxmas  11468  efgt1p2  11674  efgt1p  11675  efi4p  11696  resin4p  11697  recos4p  11698  sinbnd  11731  cosbnd  11732  dvdsval2  11768  zdvdsdc  11790  dvdsmul2  11792  dvdsmulcr  11799  dvdsabseq  11823  divconjdvds  11825  alzdvds  11830  fzo0dvdseq  11833  odd2np1lem  11847  mod2eq1n2dvds  11854  flodddiv4  11909  flodddiv4t2lthalf  11912  gcdmndc  11915  gcd0id  11950  gcd1  11958  dfgcd2  11985  gcdmultiple  11991  gcdmultiplez  11992  dvdssq  12002  lcmmndc  12032  lcm0val  12035  dvdslcm  12039  lcmeq0  12041  lcmgcd  12048  lcmdvds  12049  lcmid  12050  lcm1  12051  cncongr2  12074  isprm3  12088  prm2orodd  12096  sqrt2irrap  12150  phiprm  12193  pc0  12274  pcdvdstr  12296  unennn  12368  ennnfonelemim  12395  ctinfom  12399  ctinf  12401  enctlem  12403  elrestr  12631  mulg1  12866  mulgnegnn  12869  0opn  13137  topopn  13139  tgval  13182  tgvalex  13183  0cld  13245  ntropn  13250  ntrtop  13261  ntr0  13267  neipsm  13287  rest0  13312  xmetres  13515  metres  13516  mopnex  13638  tgioo  13679  cnlimcim  13773  cnlimc  13774  dvfre  13807  dveflem  13820  dvef  13821  efcn  13822  sin2pim  13867  cos2pim  13868  sinmpi  13869  cosmpi  13870  sinppi  13871  cosppi  13872  efimpi  13873  sincosq1lem  13879  sincosq2sgn  13881  sincosq3sgn  13882  sincosq4sgn  13883  sinq12gt0  13884  sinq34lt0t  13885  sincosq1eq  13893  abssinper  13900  logrpap0b  13930  loglt1b  13947  rpcxp0  13952  rpcxp1  13953  rpcxpsqrt  13975  logsqrt  13976  rprelogbdiv  14008  lgs0  14047  lgs2  14051  lgsneg  14058  lgsdilem  14061  lgsdir2lem2  14063  lgsdir2lem4  14065  lgsdir2lem5  14066  lgsne0  14072  bj-inf2vnlem1  14344  pwle2  14370  pwf1oexmid  14371  exmid1stab  14372  nninfsellemeqinf  14388  sbthom  14397  iswomninnlem  14420  redc0  14428
  Copyright terms: Public domain W3C validator