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  1340  equs4  1736  sb4bor  1846  elvd  2765  eueq2dc  2934  sbcgf  3054  csbconstgf  3094  sbcnestg  3135  csbnestg  3136  csbnest1g  3137  ssindif0im  3507  mpteq1  4114  iinexgm  4184  exmid1stab  4238  mss  4256  eusv2nf  4488  eldifpw  4509  ordtriexmid  4554  onsucsssucexmid  4560  ordsucunielexmid  4564  nn0suc  4637  xpss1  4770  xpiindim  4800  reldm0  4881  elrnmpt1s  4913  resdm  4982  resid  5000  eliniseg  5036  trinxp  5060  inimasn  5084  ssrnres  5109  cnveq0  5123  coi2  5183  relrelss  5193  funcnvres  5328  funimaex  5340  fnresin1  5369  fnresin2  5370  fresin  5433  dffv3g  5551  ssimaex  5619  dmfco  5626  fvmpt  5635  fsn  5731  fsn2  5733  elabrex  5801  elabrexg  5802  f1elima  5817  2ndconst  6277  tposfun  6315  tpostpos2  6320  tfrexlem  6389  tfri3  6422  rdgruledefgg  6430  rdgss  6438  frecsuclem  6461  frecrdg  6463  oa0  6512  om0  6513  oei0  6514  oav2  6518  oa1suc  6522  nnmsucr  6543  nnm1  6580  nnm2  6581  ecelqsg  6644  ecidg  6655  xpider  6662  qsel  6668  mapdm0  6719  map0e  6742  mapsnconst  6750  ixpsnf1o  6792  map1  6868  xp1en  6879  xpcomco  6882  xpmapenlem  6907  findcard2s  6948  findcard2d  6949  findcard2sd  6950  exmidpw  6966  residfi  7001  fidcenumlemr  7016  sbthlem7  7024  eqinfti  7081  djueq1  7101  omp1eomlem  7155  endjusym  7157  eninl  7158  eninr  7159  difinfsn  7161  finomni  7201  pm54.43  7252  exmidonfinlem  7255  2onetap  7317  mulidpi  7380  nlt1pig  7403  indpi  7404  halfnqq  7472  archnqq  7479  prarloclemarch  7480  prarloclemarch2  7481  nnnq  7484  nq0a0  7519  addpinq1  7526  prarloclemlt  7555  prarloclemlo  7556  prarloclem3  7559  prarloclemcalc  7564  nqprm  7604  addnqpr1  7624  1idprl  7652  1idpru  7653  1idpr  7654  recexprlem1ssl  7695  recexprlem1ssu  7696  ltmprr  7704  0idsr  7829  1idsr  7830  00sr  7831  pn0sr  7833  negexsr  7834  recexgt0sr  7835  ltm1sr  7839  archsr  7844  prsrcl  7846  prsradd  7848  mappsrprg  7866  map2psrprg  7867  elrealeu  7891  pitonnlem1p1  7908  peano2nnnn  7915  ax1rid  7939  axcnre  7943  peano5nnnn  7954  peano2cn  8156  peano2re  8157  addlid  8160  subid  8240  subid1  8241  negid  8268  negeq0  8275  peano2cnm  8287  peano2rem  8288  mul01  8410  lt0neg1  8489  le0neg1  8491  recexre  8599  inelr  8605  rimul  8606  reapmul1  8616  apsqgt0  8622  mulge0  8640  negap0  8651  divvalap  8695  rerecclap  8751  div2negap  8756  divgt0i2i  8938  peano5nni  8987  nnge1  9007  times2  9113  addltmul  9222  nn0p1nn  9282  peano2nn0  9283  nn0lele2xi  9294  znnnlt1  9368  nn0lt10b  9400  prime  9419  msqznn  9420  zeo  9425  elnn1uz2  9675  qreccl  9710  qdivcl  9711  irrmul  9715  rphalfcl  9750  rpnegap  9755  zgt1rpn0n1  9764  ltpnf  9849  nltmnf  9857  pnfge  9858  xlt0neg1  9907  xle0neg1  9909  xaddpnf1  9915  xaddmnf1  9917  xaddid1  9931  xsubge0  9950  xleaddadd  9956  elioopnf  10036  elicopnf  10038  iccshftri  10064  iccshftli  10066  iccdili  10068  icccntri  10070  fzprval  10151  fzofzp1  10297  fzostep1  10307  flqge0nn0  10365  flqge1nn  10366  fldiv4p1lem1div2  10377  exp1  10619  qexpclz  10634  nn0sqcl  10640  expeq0  10644  expubnd  10670  sqval  10671  sqeq0  10676  resqcl  10681  zsqcl  10684  iexpcyc  10718  binom21  10726  bcnn  10831  bcn2  10838  bcn2p1  10844  bcnm1  10846  fihasheq0  10867  hashsng  10872  fihashen1  10873  fimaxq  10901  iswrddm0  10941  shftfibg  10967  shftfib  10970  reim0  11008  imval2  11041  cjap0  11054  cjne0  11055  rexuz3  11137  resqrexlemover  11157  abssq  11228  nn0abscl  11232  nnabscl  11247  abs2dif  11253  max0addsup  11366  climshft  11450  bcxmas  11635  efgt1p2  11841  efgt1p  11842  efi4p  11863  resin4p  11864  recos4p  11865  sinbnd  11898  cosbnd  11899  dvdsval2  11936  zdvdsdc  11958  dvdsmul2  11960  dvdsmulcr  11967  dvdsabseq  11992  divconjdvds  11994  alzdvds  11999  fzo0dvdseq  12002  odd2np1lem  12016  mod2eq1n2dvds  12023  flodddiv4  12078  flodddiv4t2lthalf  12081  gcdmndc  12084  gcd0id  12119  gcd1  12127  dfgcd2  12154  gcdmultiple  12160  gcdmultiplez  12161  dvdssq  12171  lcmmndc  12203  lcm0val  12206  dvdslcm  12210  lcmeq0  12212  lcmgcd  12219  lcmdvds  12220  lcmid  12221  lcm1  12222  cncongr2  12245  isprm3  12259  prm2orodd  12267  sqrt2irrap  12321  phiprm  12364  pc0  12445  pcxqcl  12453  pcdvdstr  12468  unennn  12557  ennnfonelemim  12584  ctinfom  12588  ctinf  12590  enctlem  12592  elrestr  12861  tgval  12876  tgvalex  12877  xpsfrnel  12930  xpsfeq  12931  xpscf  12933  mulg1  13202  mulgnegnn  13205  ghmghmrn  13336  subrngintm  13711  subrgintm  13742  lsp0  13922  mulgrhm2  14109  zlmlemg  14127  zlmsca  14131  0opn  14185  topopn  14187  0cld  14291  ntropn  14296  ntrtop  14307  ntr0  14313  neipsm  14333  rest0  14358  xmetres  14561  metres  14562  mopnex  14684  tgioo  14733  cnlimcim  14850  cnlimc  14851  dvfre  14889  dveflem  14905  dvef  14906  efcn  14944  sin2pim  14989  cos2pim  14990  sinmpi  14991  cosmpi  14992  sinppi  14993  cosppi  14994  efimpi  14995  sincosq1lem  15001  sincosq2sgn  15003  sincosq3sgn  15004  sincosq4sgn  15005  sinq12gt0  15006  sinq34lt0t  15007  sincosq1eq  15015  abssinper  15022  logrpap0b  15052  loglt1b  15069  rpcxp0  15074  rpcxp1  15075  rpcxpsqrt  15097  logsqrt  15098  rprelogbdiv  15130  lgs0  15170  lgs2  15174  lgsneg  15181  lgsdilem  15184  lgsdir2lem2  15186  lgsdir2lem4  15188  lgsdir2lem5  15189  lgsne0  15195  2lgslem1a2  15244  2lgslem1c  15247  bj-inf2vnlem1  15532  pwle2  15559  pwf1oexmid  15560  nninfsellemeqinf  15576  sbthom  15586  iswomninnlem  15609  redc0  15617
  Copyright terms: Public domain W3C validator