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

Theorem mp2an 426
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 424 . 2 (𝜓𝜒)
51, 4ax-mp 5 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:  mp4an  427  jaoi  716  mp3an  1337  barbara  2124  eqeq12i  2191  vtocl2  2792  spc2ev  2833  sbc2ie  3034  csbieb  3098  sseq12i  3183  uneq12i  3287  ineq12i  3334  ifssun  3548  nelpri  3615  ralpr  3646  rexpr  3647  preq12i  3673  dfop  3775  opeq12i  3781  breq12i  4009  mpteq2ia  4086  exmidundif  4203  exmidundifim  4204  opex  4225  opi2  4229  opth2  4236  opeqsn  4248  opeqpr  4249  uniop  4251  opelopaba  4262  braba  4263  opelopab  4267  brab  4268  opelopabaf  4269  unex  4437  snnex  4444  op1stb  4474  ifelpwun  4479  onun2i  4486  onsucssi  4501  ontriexmidim  4517  ontr2exmid  4520  onsucsssucexmid  4522  onsucelsucexmid  4525  opthreg  4551  tfis  4578  finds  4595  finds2  4596  nnregexmid  4616  xpeq12i  4644  opelvv  4672  eqrelriiv  4716  eqrelrdv  4718  xpss  4730  xpex  4737  relop  4772  brco  4793  opelcnv  4804  brcnv  4805  asymref  5009  codir  5012  ssrnres  5066  dmprop  5098  dfco2  5123  cossxp  5146  cocnvss  5149  coex  5169  funsn  5259  fnsn  5265  feq23i  5355  resasplitss  5390  fabex  5399  fvex  5530  xpsn  5687  fmptap  5701  opabex  5735  acexmidlemv  5866  oveq12i  5880  oprabid  5900  oprabss  5954  caovcom  6025  opabex3  6116  iunex  6117  oprabex  6122  ofmres  6130  op1st  6140  op2nd  6141  fo1st  6151  fo2nd  6152  mpoex  6208  1stconst  6215  2ndconst  6216  algrflem  6223  dftpos4  6257  tpostpos  6258  tpossym  6270  frecex  6388  frecfnom  6395  sucinc  6439  fnoei  6446  oeiexg  6447  nnacli  6476  nnmcli  6477  elec  6567  ecovcom  6635  ecovass  6637  ecovdi  6639  fnmap  6648  mapval  6653  elmap  6670  elpm  6672  elpm2  6673  map0  6682  ixpconst  6701  entri  6779  endisj  6817  xpcomco  6819  phplem2  6846  ssfiexmid  6869  domfiexmid  6871  unfiexmid  6910  unfiin  6918  inresflem  7052  casefun  7077  caserel  7079  caseinj  7081  omp1eomlem  7086  omp1eom  7087  endjusym  7088  djufun  7096  djuinj  7098  ctssdccl  7103  ctssdclemr  7104  nninfex  7113  infnninf  7115  fodjuomnilemdc  7135  ctssexmid  7141  exmidonfinlem  7185  dju1p1e2  7189  exmidfodomrlemr  7194  exmidfodomrlemrALT  7195  exmidaclem  7200  pw1dom2  7219  onntri35  7229  onntri45  7233  1lt2pi  7317  indpi  7319  1nq  7343  rec1nq  7372  1lt2nq  7383  ltaddnq  7384  halfnqq  7387  prarloclemarch2  7396  prarloclemlt  7470  prarloclemcalc  7479  genpelxp  7488  ltexprlempr  7585  recexprlempr  7609  cauappcvgprlemcl  7630  cauappcvgprlemladd  7635  caucvgprlemcl  7653  caucvgprprlemcl  7681  suplocexprlemell  7690  suplocexprlemdisj  7697  suplocexprlemub  7700  0r  7727  1sr  7728  m1r  7729  m1p1sr  7737  m1m1sr  7738  0lt1sr  7742  1ne0sr  7743  1idsr  7745  recexgt0sr  7750  prsradd  7763  caucvgsrlemoffres  7777  caucvgsr  7779  mappsrprg  7781  map2psrprg  7782  pitonnlem1p1  7823  pitonnlem2  7824  pitoregt0  7826  peano2nnnn  7830  axi2m1  7852  axprecex  7857  axcnre  7858  nnindnn  7870  nntopi  7871  0cn  7927  addcli  7939  mulcli  7940  mulcomi  7941  readdcli  7948  remulcli  7949  rexpssxrxp  7979  ltrelxr  7995  gtneii  8030  lttri3i  8032  letri3i  8033  ltnsymi  8034  lenlti  8035  ltlei  8036  mulgt0i  8044  mulgt0ii  8045  0lt1  8061  addcomi  8078  pncan3oi  8150  resubcli  8197  subcli  8210  pncan3i  8211  negsubi  8212  subnegi  8213  subeq0i  8214  neg11i  8215  negcon1i  8216  negcon2i  8217  mulneg1i  8338  mulneg2i  8339  mul2negi  8340  addgt0ii  8425  ltnegi  8427  lenegi  8428  ltnegcon2i  8429  lesub0i  8430  ltaddposi  8431  posdifi  8432  ltnegcon1i  8433  lenegcon1i  8434  subge0i  8435  1ap0  8524  ltapii  8569  recrecapi  8677  dividapi  8678  div0api  8679  rec11apii  8694  divdiv32api  8700  recgt0ii  8840  ltrecii  8851  ltdiv23ii  8860  sup3exmid  8890  nnssre  8899  nnind  8911  nnmulcli  8917  nnsubi  8935  0le2  8985  1lt3  9066  2lt4  9068  1lt4  9069  3lt5  9071  2lt5  9072  1lt5  9073  4lt6  9075  3lt6  9076  2lt6  9077  1lt6  9078  5lt7  9080  4lt7  9081  3lt7  9082  2lt7  9083  1lt7  9084  6lt8  9086  5lt8  9087  4lt8  9088  3lt8  9089  2lt8  9090  1lt8  9091  7lt9  9093  6lt9  9094  5lt9  9095  4lt9  9096  3lt9  9097  2lt9  9098  1lt9  9099  2muline0  9120  nn0addcli  9189  nn0mulcli  9190  nn0addge1i  9200  nn0addge2i  9201  dfz2  9301  halfnz  9325  9p1e10  9362  numnncl  9369  numltc  9385  le9lt10  9386  nummac  9404  8lt10  9491  7lt10  9492  6lt10  9493  5lt10  9494  4lt10  9495  3lt10  9496  2lt10  9497  1lt10  9498  eluzaddi  9530  eluzsubi  9531  eluz2nn  9542  eluz4eluz2  9543  uzuzle23  9547  eluzge3nn  9548  divfnzn  9597  elq  9598  qreccl  9618  xrltnr  9753  mnfltpnf  9759  xaddmnf1  9822  pnfaddmnf  9824  mnfaddpnf  9825  xrex  9830  xaddid1  9836  xsubge0  9855  xposdif  9856  xleaddadd  9861  elicc2i  9913  ioomax  9922  iccmax  9923  ioopos  9924  elxrge0  9952  iccshftri  9969  iccshftli  9971  iccdili  9973  icccntri  9975  unitssre  9979  fz10  10019  fzpreddisj  10044  fz0to4untppr  10097  dfrp2  10237  fldiv4p1lem1div2  10278  frecfzennn  10399  fnn0nninf  10410  fxnn0nninf  10411  0tonninf  10412  1tonninf  10413  m1expcl2  10515  m1expcl  10516  nn0expcli  10519  sqmuli  10575  cu2  10591  i3  10594  subsqi  10602  binom2subi  10608  bcpasc  10717  4bc2eq6  10725  hashinfom  10729  prhash2ex  10760  hashp1i  10761  rei  10879  imi  10880  readdi  10908  imaddi  10909  remuli  10910  immuli  10911  cjaddi  10912  cjmuli  10913  ipcni  10914  crrei  10916  crimi  10917  rexfiuz  10969  sqrt1  11026  sqrt4  11027  sqrt9  11028  abs1  11052  sqrtmulii  11114  abslti  11118  abslei  11119  abssubi  11130  absmuli  11131  sqabsaddi  11132  sqabssubi  11133  abstrii  11135  fimaxre2  11206  climz  11271  abscn2  11294  recn2  11296  imcn2  11297  climabs  11299  climre  11301  climim  11302  fsumcnv  11416  fsumrelem  11450  fsumre  11451  fsumim  11452  arisum2  11478  expcnv  11483  geo2sum2  11494  geo2lim  11495  0.999...  11500  geoihalfsum  11501  fprodcnv  11604  fprodge0  11616  fprodge1  11618  ege2le3  11650  ef0  11651  reeff1  11679  tan0  11710  ef01bndlem  11735  sin01bnd  11736  cos01bnd  11737  cos1bnd  11738  cos2bnd  11739  sin01gt0  11740  cos01gt0  11741  sin02gt0  11742  sincos1sgn  11743  sincos2sgn  11744  cos12dec  11746  egt2lt3  11758  epos  11759  ene1  11763  eap1  11764  3dvdsdec  11840  3dvds2dec  11841  odd2np1lem  11847  n2dvds1  11887  z4even  11891  ndvdsi  11908  flodddiv4  11909  gcd0val  11931  6gcd4e2  11966  3lcm2e6woprm  12056  6lcm4e12  12057  3lcm2e6  12130  sqrt2irrlem  12131  phimullem  12195  pockthi  12326  xpnnen  12365  xpomen  12366  ennnfonelemj0  12372  ennnfonelem0  12376  ennnfonelemhf1o  12384  exmidunben  12397  qnnen  12402  unct  12413  setscom  12472  strleun  12532  ismgm  12655  fn0g  12673  issgrp  12688  ismnddef  12698  isring  12996  mgpf  13007  txtopi  13394  txunii  13397  upxp  13405  uptx  13407  cnmpt1st  13421  cnmpt2nd  13422  txswaphmeolem  13453  qtopbasss  13654  cnmet  13663  cnopncntop  13670  remet  13673  blssioo  13678  tgqioo  13680  tgioo2cntop  13682  divcnap  13688  abscncf  13705  recncf  13706  imcncf  13707  cjcncf  13708  mulc1cncf  13709  cncfcn1cntop  13714  cdivcncfap  13720  expcncf  13725  cnrehmeocntop  13726  limccnp2lem  13778  limccnp2cntop  13779  dvcnp2cntop  13796  dvaddxxbr  13798  dvmulxxbr  13799  dvcoapbr  13804  dvrecap  13810  dveflem  13820  dvef  13821  sincn  13823  coscn  13824  reeff1oleme  13826  reeff1o  13827  cosz12  13834  sin0pilem1  13835  sin0pilem2  13836  pipos  13842  sinhalfpilem  13845  sincosq1lem  13879  sincosq1sgn  13880  sincosq2sgn  13881  sincosq3sgn  13882  sincosq4sgn  13883  sinq12gt0  13884  cosq14gt0  13886  cosq23lt0  13887  coseq0q4123  13888  coseq00topi  13889  coseq0negpitopi  13890  tangtx  13892  sincos4thpi  13894  tan4thpi  13895  sincos6thpi  13896  pigt3  13898  cosordlem  13903  cosq34lt1  13904  cos02pilt1  13905  cos0pilt1  13906  ioocosf1o  13908  negpitopissre  13909  log1  13920  loge  13921  2logb9irr  14022  sqrt2cxp2logb9e3  14026  2logb9irrap  14028  lgsdir2lem2  14063  lgsdir2lem3  14064  2sqlem9  14093  2sqlem10  14094  ex-fl  14099  ex-ceil  14100  ex-bc  14103  ex-dvds  14104  ex-gcd  14105  bj-charfunbi  14185  bj-unex  14293  bj-nn0suc0  14324  bj-nntrans  14325  bj-nnelirr  14327  012of  14367  2o01f  14368  pwle2  14370  nnsf  14377  peano3nninf  14379  exmidsbthrlem  14393  sbthom  14397  isomninnlem  14401  iooref1o  14405  trilpolemisumle  14409  trilpolemeq1  14411  trilpolemlt1  14412  apdiff  14419  iswomninnlem  14420  iswomni0  14422  ismkvnnlem  14423  dceqnconst  14430  dcapnconst  14431  nconstwlpolemgt0  14434  taupi  14441
  Copyright terms: Public domain W3C validator