ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  mpan2 GIF 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 𝜓
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 412 1 (𝜑𝜒)
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  1655  sb4bor  1758  eueq2dc  2774  sbcgf  2890  csbconstgf  2928  sbcnestg  2964  csbnestg  2965  csbnest1g  2966  ssindif0im  3319  mpteq1  3882  iinexgm  3949  mss  4009  eusv2nf  4234  eldifpw  4254  ordtriexmid  4293  onsucsssucexmid  4298  ordsucunielexmid  4302  nn0suc  4373  xpss1  4496  xpiindim  4521  reldm0  4601  elrnmpt1s  4632  resdm  4697  resid  4712  eliniseg  4745  trinxp  4768  inimasn  4791  ssrnres  4813  cnveq0  4827  coi2  4887  relrelss  4894  funcnvres  5023  funimaex  5035  fnresin1  5064  fnresin2  5065  fresin  5119  dffv3g  5226  ssimaex  5287  dmfco  5294  fvmpt  5302  fsn  5388  fsn2  5390  elabrex  5450  f1elima  5465  2ndconst  5895  tposfun  5930  tpostpos2  5935  tfrexlem  6004  tfri3  6037  rdgruledefgg  6045  rdgss  6053  frecsuclem  6076  frecrdg  6078  oa0  6122  om0  6123  oei0  6124  oav2  6128  oa1suc  6132  nnmsucr  6153  nnm1  6185  nnm2  6186  ecelqsg  6247  ecidg  6258  xpiderm  6265  qsel  6271  xp1en  6389  xpcomco  6392  findcard2s  6447  findcard2d  6448  findcard2sd  6449  eqinfti  6528  djueq1  6550  pm54.43  6588  mulidpi  6640  nlt1pig  6663  indpi  6664  halfnqq  6732  archnqq  6739  prarloclemarch  6740  prarloclemarch2  6741  nnnq  6744  nq0a0  6779  addpinq1  6786  prarloclemlt  6815  prarloclemlo  6816  prarloclem3  6819  prarloclemcalc  6824  nqprm  6864  addnqpr1  6884  1idprl  6912  1idpru  6913  1idpr  6914  recexprlem1ssl  6955  recexprlem1ssu  6956  ltmprr  6964  0idsr  7076  1idsr  7077  00sr  7078  pn0sr  7080  negexsr  7081  recexgt0sr  7082  archsr  7090  prsrcl  7092  prsradd  7094  elrealeu  7130  pitonnlem1p1  7146  peano2nnnn  7153  ax1rid  7175  axcnre  7179  peano5nnnn  7190  peano2cn  7380  peano2re  7381  addid2  7384  subid  7464  subid1  7465  negid  7492  negeq0  7499  peano2cnm  7511  peano2rem  7512  mul01  7630  lt0neg1  7709  le0neg1  7711  recexre  7815  inelr  7821  rimul  7822  reapmul1  7832  apsqgt0  7838  mulge0  7856  negap0  7866  divvalap  7899  rerecclap  7955  div2negap  7960  divgt0i2i  8132  peano5nni  8179  nnge1  8199  times2  8298  addltmul  8404  nn0p1nn  8464  peano2nn0  8465  nn0lele2xi  8476  znnnlt1  8550  nn0lt10b  8579  prime  8597  msqznn  8598  zeo  8603  elnn1uz2  8845  qreccl  8878  qdivcl  8879  irrmul  8883  rphalfcl  8912  rpnegap  8917  ltpnf  9002  nltmnf  9009  pnfge  9010  xlt0neg1  9051  xle0neg1  9053  elioopnf  9136  elicopnf  9138  iccshftri  9163  iccshftli  9165  iccdili  9167  icccntri  9169  fzprval  9245  fzofzp1  9383  fzostep1  9393  flqge0nn0  9445  flqge1nn  9446  fldiv4p1lem1div2  9457  expivallem  9644  expival  9645  exp1  9649  qexpclz  9664  nn0sqcl  9670  expeq0  9674  expubnd  9700  sqval  9701  sqeq0  9706  resqcl  9710  zsqcl  9713  iexpcyc  9746  binom21  9753  bcnn  9851  bcn2  9858  bcn2p1  9864  bcnm1  9866  fihasheq0  9888  hashsng  9892  fihashen1  9893  shftfibg  9927  shftfib  9930  reim0  9967  imval2  10000  cjap0  10013  cjne0  10014  rexuz3  10095  resqrexlemover  10115  abs00  10169  abssq  10186  nn0abscl  10190  nnabscl  10205  abs2dif  10211  max0addsup  10324  climshft  10362  dvdsval2  10424  zdvdsdc  10442  dvdsmul2  10444  dvdsmulcr  10451  dvdsabseq  10473  divconjdvds  10475  alzdvds  10480  fzo0dvdseq  10483  odd2np1lem  10497  mod2eq1n2dvds  10504  flodddiv4  10559  flodddiv4t2lthalf  10562  gcdmndc  10565  gcd0id  10595  gcd1  10603  dfgcd2  10628  gcdmultiple  10634  gcdmultiplez  10635  dvdssq  10645  lcmmndc  10669  lcm0val  10672  dvdslcm  10676  lcmeq0  10678  lcmgcd  10685  lcmdvds  10686  lcmid  10687  lcm1  10688  cncongr2  10711  isprm3  10725  prm2orodd  10733  sqrt2irrap  10783  phiprm  10824  unennn  10835  bj-inf2vnlem1  11050
  Copyright terms: Public domain W3C validator