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

Theorem mp2an 423
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
Hypotheses
Ref Expression
mp2an.1 𝜑
mp2an.2 𝜓
mp2an.3 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
mp2an 𝜒

Proof of Theorem mp2an
StepHypRef Expression
1 mp2an.2 . 2 𝜓
2 mp2an.1 . . 3 𝜑
3 mp2an.3 . . 3 ((𝜑𝜓) → 𝜒)
42, 3mpan 421 . 2 (𝜓𝜒)
51, 4ax-mp 5 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:  mp4an  424  jaoi  706  mp3an  1316  barbara  2098  eqeq12i  2154  vtocl2  2744  spc2ev  2784  sbc2ie  2983  csbieb  3045  sseq12i  3129  uneq12i  3232  ineq12i  3279  nelpri  3555  ralpr  3585  rexpr  3586  preq12i  3612  dfop  3711  opeq12i  3717  breq12i  3945  mpteq2ia  4021  exmidundif  4136  exmidundifim  4137  opex  4158  opi2  4162  opth2  4169  opeqsn  4181  opeqpr  4182  uniop  4184  opelopaba  4195  braba  4196  opelopab  4200  brab  4201  opelopabaf  4202  unex  4369  snnex  4376  op1stb  4406  onun2i  4414  onsucssi  4429  ontr2exmid  4447  onsucsssucexmid  4449  onsucelsucexmid  4452  opthreg  4478  tfis  4504  finds  4521  finds2  4522  nnregexmid  4541  xpeq12i  4568  opelvv  4596  eqrelriiv  4640  eqrelrdv  4642  xpss  4654  xpex  4661  relop  4696  brco  4717  opelcnv  4728  brcnv  4729  asymref  4931  codir  4934  ssrnres  4988  dmprop  5020  dfco2  5045  cossxp  5068  cocnvss  5071  coex  5091  funsn  5178  fnsn  5184  feq23i  5274  resasplitss  5309  fabex  5318  fvex  5448  xpsn  5603  fmptap  5617  opabex  5651  acexmidlemv  5779  oveq12i  5793  oprabid  5810  oprabss  5864  caovcom  5935  opabex3  6027  iunex  6028  oprabex  6033  ofmres  6041  op1st  6051  op2nd  6052  fo1st  6062  fo2nd  6063  mpoex  6118  1stconst  6125  2ndconst  6126  algrflem  6133  dftpos4  6167  tpostpos  6168  tpossym  6180  frecex  6298  frecfnom  6305  sucinc  6348  fnoei  6355  oeiexg  6356  nnacli  6385  nnmcli  6386  elec  6475  ecovcom  6543  ecovass  6545  ecovdi  6547  fnmap  6556  mapval  6561  elmap  6578  elpm  6580  elpm2  6581  map0  6590  ixpconst  6609  entri  6687  endisj  6725  xpcomco  6727  phplem2  6754  ssfiexmid  6777  domfiexmid  6779  unfiexmid  6813  unfiin  6821  inresflem  6952  casefun  6977  caserel  6979  caseinj  6981  omp1eomlem  6986  omp1eom  6987  endjusym  6988  djufun  6996  djuinj  6998  ctssdccl  7003  ctssdclemr  7004  fodjuomnilemdc  7023  ctssexmid  7031  exmidonfinlem  7065  dju1p1e2  7069  exmidfodomrlemr  7074  exmidfodomrlemrALT  7075  exmidaclem  7080  1lt2pi  7171  indpi  7173  1nq  7197  rec1nq  7226  1lt2nq  7237  ltaddnq  7238  halfnqq  7241  prarloclemarch2  7250  prarloclemlt  7324  prarloclemcalc  7333  genpelxp  7342  ltexprlempr  7439  recexprlempr  7463  cauappcvgprlemcl  7484  cauappcvgprlemladd  7489  caucvgprlemcl  7507  caucvgprprlemcl  7535  suplocexprlemell  7544  suplocexprlemdisj  7551  suplocexprlemub  7554  0r  7581  1sr  7582  m1r  7583  m1p1sr  7591  m1m1sr  7592  0lt1sr  7596  1ne0sr  7597  1idsr  7599  recexgt0sr  7604  prsradd  7617  caucvgsrlemoffres  7631  caucvgsr  7633  mappsrprg  7635  map2psrprg  7636  pitonnlem1p1  7677  pitonnlem2  7678  pitoregt0  7680  peano2nnnn  7684  axi2m1  7706  axprecex  7711  axcnre  7712  nnindnn  7724  nntopi  7725  0cn  7781  addcli  7793  mulcli  7794  mulcomi  7795  readdcli  7802  remulcli  7803  rexpssxrxp  7833  ltrelxr  7848  gtneii  7882  lttri3i  7884  letri3i  7885  ltnsymi  7886  lenlti  7887  ltlei  7888  mulgt0i  7896  mulgt0ii  7897  0lt1  7912  addcomi  7929  pncan3oi  8001  resubcli  8048  subcli  8061  pncan3i  8062  negsubi  8063  subnegi  8064  subeq0i  8065  neg11i  8066  negcon1i  8067  negcon2i  8068  mulneg1i  8189  mulneg2i  8190  mul2negi  8191  addgt0ii  8276  ltnegi  8278  lenegi  8279  ltnegcon2i  8280  lesub0i  8281  ltaddposi  8282  posdifi  8283  ltnegcon1i  8284  lenegcon1i  8285  subge0i  8286  1ap0  8375  ltapii  8420  recrecapi  8527  dividapi  8528  div0api  8529  rec11apii  8544  divdiv32api  8550  recgt0ii  8688  ltrecii  8699  ltdiv23ii  8708  sup3exmid  8738  nnssre  8747  nnind  8759  nnmulcli  8765  nnsubi  8783  0le2  8833  1lt3  8914  2lt4  8916  1lt4  8917  3lt5  8919  2lt5  8920  1lt5  8921  4lt6  8923  3lt6  8924  2lt6  8925  1lt6  8926  5lt7  8928  4lt7  8929  3lt7  8930  2lt7  8931  1lt7  8932  6lt8  8934  5lt8  8935  4lt8  8936  3lt8  8937  2lt8  8938  1lt8  8939  7lt9  8941  6lt9  8942  5lt9  8943  4lt9  8944  3lt9  8945  2lt9  8946  1lt9  8947  2muline0  8968  nn0addcli  9037  nn0mulcli  9038  nn0addge1i  9048  nn0addge2i  9049  dfz2  9146  halfnz  9170  9p1e10  9207  numnncl  9214  numltc  9230  le9lt10  9231  nummac  9249  8lt10  9336  7lt10  9337  6lt10  9338  5lt10  9339  4lt10  9340  3lt10  9341  2lt10  9342  1lt10  9343  eluzaddi  9375  eluzsubi  9376  eluz2nn  9387  eluz4eluz2  9388  uzuzle23  9392  eluzge3nn  9393  divfnzn  9439  elq  9440  qreccl  9460  xrltnr  9595  mnfltpnf  9600  xaddmnf1  9660  pnfaddmnf  9662  mnfaddpnf  9663  xrex  9668  xaddid1  9674  xsubge0  9693  xposdif  9694  xleaddadd  9699  elicc2i  9751  ioomax  9760  iccmax  9761  ioopos  9762  elxrge0  9790  iccshftri  9807  iccshftli  9809  iccdili  9811  icccntri  9813  unitssre  9817  fz10  9856  fzpreddisj  9881  fldiv4p1lem1div2  10108  frecfzennn  10229  fnn0nninf  10240  fxnn0nninf  10241  0tonninf  10242  1tonninf  10243  m1expcl2  10345  m1expcl  10346  nn0expcli  10349  sqmuli  10405  cu2  10421  i3  10424  subsqi  10432  binom2subi  10437  bcpasc  10543  4bc2eq6  10551  hashinfom  10555  prhash2ex  10586  hashp1i  10587  rei  10702  imi  10703  readdi  10731  imaddi  10732  remuli  10733  immuli  10734  cjaddi  10735  cjmuli  10736  ipcni  10737  crrei  10739  crimi  10740  rexfiuz  10792  sqrt1  10849  sqrt4  10850  sqrt9  10851  abs1  10875  sqrtmulii  10937  abslti  10941  abslei  10942  abssubi  10953  absmuli  10954  sqabsaddi  10955  sqabssubi  10956  abstrii  10958  fimaxre2  11029  climz  11092  abscn2  11115  recn2  11117  imcn2  11118  climabs  11120  climre  11122  climim  11123  fsumcnv  11237  fsumrelem  11271  fsumre  11272  fsumim  11273  arisum2  11299  expcnv  11304  geo2sum2  11315  geo2lim  11316  0.999...  11321  geoihalfsum  11322  ege2le3  11412  ef0  11413  reeff1  11441  tan0  11472  ef01bndlem  11497  sin01bnd  11498  cos01bnd  11499  cos1bnd  11500  cos2bnd  11501  sin01gt0  11502  cos01gt0  11503  sin02gt0  11504  sincos1sgn  11505  sincos2sgn  11506  cos12dec  11508  egt2lt3  11520  epos  11521  ene1  11525  eap1  11526  3dvdsdec  11596  3dvds2dec  11597  odd2np1lem  11603  n2dvds1  11643  z4even  11647  ndvdsi  11664  flodddiv4  11665  gcd0val  11683  6gcd4e2  11717  3lcm2e6woprm  11801  6lcm4e12  11802  3lcm2e6  11872  sqrt2irrlem  11873  phimullem  11935  xpnnen  11941  xpomen  11942  ennnfonelemj0  11948  ennnfonelem0  11952  ennnfonelemhf1o  11960  exmidunben  11973  qnnen  11978  unct  11989  setscom  12036  strleun  12085  txtopi  12467  txunii  12470  upxp  12478  uptx  12480  cnmpt1st  12494  cnmpt2nd  12495  txswaphmeolem  12526  qtopbasss  12727  cnmet  12736  cnopncntop  12743  remet  12746  blssioo  12751  tgqioo  12753  tgioo2cntop  12755  divcnap  12761  abscncf  12778  recncf  12779  imcncf  12780  cjcncf  12781  mulc1cncf  12782  cncfcn1cntop  12787  cdivcncfap  12793  expcncf  12798  cnrehmeocntop  12799  limccnp2lem  12851  limccnp2cntop  12852  dvcnp2cntop  12869  dvaddxxbr  12871  dvmulxxbr  12872  dvcoapbr  12877  dvrecap  12883  dveflem  12893  dvef  12894  sincn  12896  coscn  12897  reeff1oleme  12899  reeff1o  12900  cosz12  12907  sin0pilem1  12908  sin0pilem2  12909  pipos  12915  sinhalfpilem  12918  sincosq1lem  12952  sincosq1sgn  12953  sincosq2sgn  12954  sincosq3sgn  12955  sincosq4sgn  12956  sinq12gt0  12957  cosq14gt0  12959  cosq23lt0  12960  coseq0q4123  12961  coseq00topi  12962  coseq0negpitopi  12963  tangtx  12965  sincos4thpi  12967  tan4thpi  12968  sincos6thpi  12969  pigt3  12971  cosordlem  12976  cosq34lt1  12977  cos02pilt1  12978  cos0pilt1  12979  ioocosf1o  12981  negpitopissre  12982  log1  12993  loge  12994  2logb9irr  13094  sqrt2cxp2logb9e3  13098  2logb9irrap  13100  ex-fl  13106  ex-ceil  13107  ex-bc  13110  ex-dvds  13111  ex-gcd  13112  bj-unex  13286  bj-nn0suc0  13317  bj-nntrans  13318  bj-nnelirr  13320  pw1dom2  13359  012of  13361  2o01f  13362  pwle2  13364  nnsf  13372  peano3nninf  13374  nninfex  13378  exmidsbthrlem  13390  sbthom  13394  isomninnlem  13398  trilpolemisumle  13404  trilpolemeq1  13406  trilpolemlt1  13407  apdiff  13414  iswomninnlem  13415  ismkvnnlem  13417  dcapncf  13421  iooref1o  13424  taupi  13428
  Copyright terms: Public domain W3C validator