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

Theorem mpan2 419
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 415 1 (𝜑𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 107
This theorem is referenced by:  mpanr12  433  mp3an23  1290  equs4  1686  sb4bor  1789  elvd  2663  eueq2dc  2828  sbcgf  2946  csbconstgf  2984  sbcnestg  3021  csbnestg  3022  csbnest1g  3023  ssindif0im  3390  mpteq1  3980  iinexgm  4047  mss  4116  eusv2nf  4345  eldifpw  4366  ordtriexmid  4405  onsucsssucexmid  4410  ordsucunielexmid  4414  nn0suc  4486  xpss1  4617  xpiindim  4644  reldm0  4725  elrnmpt1s  4757  resdm  4826  resid  4843  eliniseg  4877  trinxp  4900  inimasn  4924  ssrnres  4949  cnveq0  4963  coi2  5023  relrelss  5033  funcnvres  5164  funimaex  5176  fnresin1  5205  fnresin2  5206  fresin  5269  dffv3g  5383  ssimaex  5448  dmfco  5455  fvmpt  5464  fsn  5558  fsn2  5560  elabrex  5625  f1elima  5640  2ndconst  6085  tposfun  6123  tpostpos2  6128  tfrexlem  6197  tfri3  6230  rdgruledefgg  6238  rdgss  6246  frecsuclem  6269  frecrdg  6271  oa0  6319  om0  6320  oei0  6321  oav2  6325  oa1suc  6329  nnmsucr  6350  nnm1  6386  nnm2  6387  ecelqsg  6448  ecidg  6459  xpider  6466  qsel  6472  mapdm0  6523  map0e  6546  mapsnconst  6554  ixpsnf1o  6596  map1  6672  xp1en  6683  xpcomco  6686  xpmapenlem  6709  findcard2s  6750  findcard2d  6751  findcard2sd  6752  exmidpw  6768  fidcenumlemr  6809  sbthlem7  6817  eqinfti  6873  djueq1  6891  omp1eomlem  6945  endjusym  6947  eninl  6948  eninr  6949  difinfsn  6951  finomni  6978  pm54.43  7012  mulidpi  7090  nlt1pig  7113  indpi  7114  halfnqq  7182  archnqq  7189  prarloclemarch  7190  prarloclemarch2  7191  nnnq  7194  nq0a0  7229  addpinq1  7236  prarloclemlt  7265  prarloclemlo  7266  prarloclem3  7269  prarloclemcalc  7274  nqprm  7314  addnqpr1  7334  1idprl  7362  1idpru  7363  1idpr  7364  recexprlem1ssl  7405  recexprlem1ssu  7406  ltmprr  7414  0idsr  7539  1idsr  7540  00sr  7541  pn0sr  7543  negexsr  7544  recexgt0sr  7545  ltm1sr  7549  archsr  7554  prsrcl  7556  prsradd  7558  mappsrprg  7576  map2psrprg  7577  elrealeu  7601  pitonnlem1p1  7618  peano2nnnn  7625  ax1rid  7649  axcnre  7653  peano5nnnn  7664  peano2cn  7861  peano2re  7862  addid2  7865  subid  7945  subid1  7946  negid  7973  negeq0  7980  peano2cnm  7992  peano2rem  7993  mul01  8115  lt0neg1  8194  le0neg1  8196  recexre  8303  inelr  8309  rimul  8310  reapmul1  8320  apsqgt0  8326  mulge0  8344  negap0  8355  divvalap  8397  rerecclap  8453  div2negap  8458  divgt0i2i  8635  peano5nni  8683  nnge1  8703  times2  8803  addltmul  8910  nn0p1nn  8970  peano2nn0  8971  nn0lele2xi  8982  znnnlt1  9056  nn0lt10b  9085  prime  9104  msqznn  9105  zeo  9110  elnn1uz2  9353  qreccl  9386  qdivcl  9387  irrmul  9391  rphalfcl  9420  rpnegap  9425  ltpnf  9518  nltmnf  9525  pnfge  9526  xlt0neg1  9572  xle0neg1  9574  xaddpnf1  9580  xaddmnf1  9582  xaddid1  9596  xsubge0  9615  xleaddadd  9621  elioopnf  9701  elicopnf  9703  iccshftri  9729  iccshftli  9731  iccdili  9733  icccntri  9735  fzprval  9813  fzofzp1  9955  fzostep1  9965  flqge0nn0  10017  flqge1nn  10018  fldiv4p1lem1div2  10029  exp1  10250  qexpclz  10265  nn0sqcl  10271  expeq0  10275  expubnd  10301  sqval  10302  sqeq0  10307  resqcl  10311  zsqcl  10314  iexpcyc  10348  binom21  10355  bcnn  10454  bcn2  10461  bcn2p1  10467  bcnm1  10469  fihasheq0  10491  hashsng  10495  fihashen1  10496  fimaxq  10524  shftfibg  10543  shftfib  10546  reim0  10584  imval2  10617  cjap0  10630  cjne0  10631  rexuz3  10713  resqrexlemover  10733  abssq  10804  nn0abscl  10808  nnabscl  10823  abs2dif  10829  max0addsup  10942  climshft  11024  bcxmas  11209  efgt1p2  11311  efgt1p  11312  efi4p  11334  resin4p  11335  recos4p  11336  sinbnd  11369  cosbnd  11370  dvdsval2  11403  zdvdsdc  11421  dvdsmul2  11423  dvdsmulcr  11430  dvdsabseq  11452  divconjdvds  11454  alzdvds  11459  fzo0dvdseq  11462  odd2np1lem  11476  mod2eq1n2dvds  11483  flodddiv4  11538  flodddiv4t2lthalf  11541  gcdmndc  11544  gcd0id  11574  gcd1  11582  dfgcd2  11609  gcdmultiple  11615  gcdmultiplez  11616  dvdssq  11626  lcmmndc  11650  lcm0val  11653  dvdslcm  11657  lcmeq0  11659  lcmgcd  11666  lcmdvds  11667  lcmid  11668  lcm1  11669  cncongr2  11692  isprm3  11706  prm2orodd  11714  sqrt2irrap  11764  phiprm  11805  unennn  11816  ennnfonelemim  11843  ctinfom  11847  ctinf  11849  enctlem  11851  ressid  11926  elrestr  12034  0opn  12079  topopn  12081  tgval  12124  tgvalex  12125  0cld  12187  ntropn  12192  ntrtop  12203  ntr0  12209  neipsm  12229  rest0  12254  xmetres  12457  metres  12458  mopnex  12580  tgioo  12621  cnlimcim  12715  cnlimc  12716  dvfre  12749  dveflem  12761  dvef  12762  efcn  12763  bj-inf2vnlem1  13002  pwle2  13027  pwf1oexmid  13028  exmid1stab  13029  nninfsellemeqinf  13046  sbthom  13055
  Copyright terms: Public domain W3C validator