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

Theorem mp2an 420
Description: An inference based on modus ponens. (Contributed by NM, 13-Apr-1995.)
Hypotheses
Ref Expression
mp2an.1  |-  ph
mp2an.2  |-  ps
mp2an.3  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
mp2an  |-  ch

Proof of Theorem mp2an
StepHypRef Expression
1 mp2an.2 . 2  |-  ps
2 mp2an.1 . . 3  |-  ph
3 mp2an.3 . . 3  |-  ( (
ph  /\  ps )  ->  ch )
42, 3mpan 418 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 5 1  |-  ch
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  421  jaoi  688  mp3an  1298  barbara  2073  eqeq12i  2129  vtocl2  2713  spc2ev  2753  sbc2ie  2950  csbieb  3009  sseq12i  3093  uneq12i  3196  ineq12i  3243  nelpri  3519  ralpr  3546  rexpr  3547  preq12i  3573  dfop  3672  opeq12i  3678  breq12i  3906  mpteq2ia  3982  exmidundif  4097  exmidundifim  4098  opex  4119  opi2  4123  opth2  4130  opeqsn  4142  opeqpr  4143  uniop  4145  opelopaba  4156  braba  4157  opelopab  4161  brab  4162  opelopabaf  4163  unex  4330  snnex  4337  op1stb  4367  onun2i  4375  onsucssi  4390  ontr2exmid  4408  onsucsssucexmid  4410  onsucelsucexmid  4413  opthreg  4439  tfis  4465  finds  4482  finds2  4483  nnregexmid  4502  xpeq12i  4529  opelvv  4557  eqrelriiv  4601  eqrelrdv  4603  xpss  4615  xpex  4622  relop  4657  brco  4678  opelcnv  4689  brcnv  4690  asymref  4892  codir  4895  ssrnres  4949  dmprop  4981  dfco2  5006  cossxp  5029  cocnvss  5032  coex  5052  funsn  5139  fnsn  5145  feq23i  5235  resasplitss  5270  fabex  5279  fvex  5407  xpsn  5562  fmptap  5576  opabex  5610  acexmidlemv  5738  oveq12i  5752  oprabid  5769  oprabss  5823  caovcom  5894  opabex3  5986  iunex  5987  oprabex  5992  ofmres  6000  op1st  6010  op2nd  6011  fo1st  6021  fo2nd  6022  mpoex  6077  1stconst  6084  2ndconst  6085  algrflem  6092  dftpos4  6126  tpostpos  6127  tpossym  6139  frecex  6257  frecfnom  6264  sucinc  6307  fnoei  6314  oeiexg  6315  nnacli  6344  nnmcli  6345  elec  6434  ecovcom  6502  ecovass  6504  ecovdi  6506  fnmap  6515  mapval  6520  elmap  6537  elpm  6539  elpm2  6540  map0  6549  ixpconst  6568  entri  6646  endisj  6684  xpcomco  6686  phplem2  6713  ssfiexmid  6736  domfiexmid  6738  unfiexmid  6772  unfiin  6780  inresflem  6911  casefun  6936  caserel  6938  caseinj  6940  omp1eomlem  6945  omp1eom  6946  endjusym  6947  djufun  6955  djuinj  6957  ctssdccl  6962  ctssdclemr  6963  fodjuomnilemdc  6982  ctssexmid  6990  dju1p1e2  7017  exmidfodomrlemr  7022  exmidfodomrlemrALT  7023  exmidaclem  7028  1lt2pi  7112  indpi  7114  1nq  7138  rec1nq  7167  1lt2nq  7178  ltaddnq  7179  halfnqq  7182  prarloclemarch2  7191  prarloclemlt  7265  prarloclemcalc  7274  genpelxp  7283  ltexprlempr  7380  recexprlempr  7404  cauappcvgprlemcl  7425  cauappcvgprlemladd  7430  caucvgprlemcl  7448  caucvgprprlemcl  7476  suplocexprlemell  7485  suplocexprlemdisj  7492  suplocexprlemub  7495  0r  7522  1sr  7523  m1r  7524  m1p1sr  7532  m1m1sr  7533  0lt1sr  7537  1ne0sr  7538  1idsr  7540  recexgt0sr  7545  prsradd  7558  caucvgsrlemoffres  7572  caucvgsr  7574  mappsrprg  7576  map2psrprg  7577  pitonnlem1p1  7618  pitonnlem2  7619  pitoregt0  7621  peano2nnnn  7625  axi2m1  7647  axprecex  7652  axcnre  7653  nnindnn  7665  nntopi  7666  0cn  7722  addcli  7734  mulcli  7735  mulcomi  7736  readdcli  7743  remulcli  7744  rexpssxrxp  7774  ltrelxr  7789  gtneii  7823  lttri3i  7825  letri3i  7826  ltnsymi  7827  lenlti  7828  ltlei  7829  mulgt0i  7837  mulgt0ii  7838  0lt1  7853  addcomi  7870  pncan3oi  7942  resubcli  7989  subcli  8002  pncan3i  8003  negsubi  8004  subnegi  8005  subeq0i  8006  neg11i  8007  negcon1i  8008  negcon2i  8009  mulneg1i  8130  mulneg2i  8131  mul2negi  8132  addgt0ii  8217  ltnegi  8219  lenegi  8220  ltnegcon2i  8221  lesub0i  8222  ltaddposi  8223  posdifi  8224  ltnegcon1i  8225  lenegcon1i  8226  subge0i  8227  1ap0  8315  ltapii  8360  recrecapi  8467  dividapi  8468  div0api  8469  rec11apii  8484  divdiv32api  8490  recgt0ii  8625  ltrecii  8636  ltdiv23ii  8645  sup3exmid  8675  nnssre  8684  nnind  8696  nnmulcli  8702  nnsubi  8720  0le2  8770  1lt3  8845  2lt4  8847  1lt4  8848  3lt5  8850  2lt5  8851  1lt5  8852  4lt6  8854  3lt6  8855  2lt6  8856  1lt6  8857  5lt7  8859  4lt7  8860  3lt7  8861  2lt7  8862  1lt7  8863  6lt8  8865  5lt8  8866  4lt8  8867  3lt8  8868  2lt8  8869  1lt8  8870  7lt9  8872  6lt9  8873  5lt9  8874  4lt9  8875  3lt9  8876  2lt9  8877  1lt9  8878  2muline0  8899  nn0addcli  8968  nn0mulcli  8969  nn0addge1i  8979  nn0addge2i  8980  dfz2  9077  halfnz  9101  9p1e10  9138  numnncl  9145  numltc  9161  le9lt10  9162  nummac  9180  8lt10  9267  7lt10  9268  6lt10  9269  5lt10  9270  4lt10  9271  3lt10  9272  2lt10  9273  1lt10  9274  eluzaddi  9304  eluzsubi  9305  eluz2nn  9316  uzuzle23  9318  eluzge3nn  9319  divfnzn  9365  elq  9366  qreccl  9386  xrltnr  9517  mnfltpnf  9522  xaddmnf1  9582  pnfaddmnf  9584  mnfaddpnf  9585  xrex  9590  xaddid1  9596  xsubge0  9615  xposdif  9616  xleaddadd  9621  elicc2i  9673  ioomax  9682  iccmax  9683  ioopos  9684  elxrge0  9712  iccshftri  9729  iccshftli  9731  iccdili  9733  icccntri  9735  unitssre  9739  fz10  9777  fzpreddisj  9802  fldiv4p1lem1div2  10029  frecfzennn  10150  fnn0nninf  10161  fxnn0nninf  10162  0tonninf  10163  1tonninf  10164  m1expcl2  10266  m1expcl  10267  nn0expcli  10270  sqmuli  10326  cu2  10342  i3  10345  subsqi  10353  binom2subi  10358  bcpasc  10463  4bc2eq6  10471  hashinfom  10475  prhash2ex  10506  hashp1i  10507  rei  10622  imi  10623  readdi  10651  imaddi  10652  remuli  10653  immuli  10654  cjaddi  10655  cjmuli  10656  ipcni  10657  crrei  10659  crimi  10660  rexfiuz  10712  sqrt1  10769  sqrt4  10770  sqrt9  10771  abs1  10795  sqrtmulii  10857  abslti  10861  abslei  10862  abssubi  10873  absmuli  10874  sqabsaddi  10875  sqabssubi  10876  abstrii  10878  fimaxre2  10949  climz  11012  abscn2  11035  recn2  11037  imcn2  11038  climabs  11040  climre  11042  climim  11043  fsumcnv  11157  fsumrelem  11191  fsumre  11192  fsumim  11193  arisum2  11219  expcnv  11224  geo2sum2  11235  geo2lim  11236  0.999...  11241  geoihalfsum  11242  ege2le3  11287  ef0  11288  reeff1  11317  tan0  11348  ef01bndlem  11373  sin01bnd  11374  cos01bnd  11375  cos1bnd  11376  cos2bnd  11377  sin01gt0  11378  cos01gt0  11379  sin02gt0  11380  sincos1sgn  11381  sincos2sgn  11382  egt2lt3  11393  epos  11394  ene1  11398  eap1  11399  3dvdsdec  11469  3dvds2dec  11470  odd2np1lem  11476  n2dvds1  11516  z4even  11520  ndvdsi  11537  flodddiv4  11538  gcd0val  11556  6gcd4e2  11590  3lcm2e6woprm  11674  6lcm4e12  11675  3lcm2e6  11745  sqrt2irrlem  11746  phimullem  11807  xpnnen  11813  xpomen  11814  ennnfonelemj0  11820  ennnfonelem0  11824  ennnfonelemhf1o  11832  exmidunben  11845  qnnen  11850  unct  11860  setscom  11905  strleun  11954  txtopi  12336  txunii  12339  upxp  12347  uptx  12349  cnmpt1st  12363  cnmpt2nd  12364  txswaphmeolem  12395  qtopbasss  12596  cnmet  12605  cnopncntop  12612  remet  12615  blssioo  12620  tgqioo  12622  tgioo2cntop  12624  divcnap  12630  abscncf  12647  recncf  12648  imcncf  12649  cjcncf  12650  mulc1cncf  12651  cncfcn1cntop  12656  cdivcncfap  12662  expcncf  12667  cnrehmeocntop  12668  limccnp2lem  12720  limccnp2cntop  12721  dvcnp2cntop  12738  dvaddxxbr  12740  dvmulxxbr  12741  dvcoapbr  12746  dvrecap  12752  dveflem  12761  dvef  12762  sincn  12764  coscn  12765  ex-fl  12771  ex-ceil  12772  ex-bc  12775  ex-dvds  12776  ex-gcd  12777  bj-unex  12951  bj-nn0suc0  12982  bj-nntrans  12983  bj-nnelirr  12985  pw1dom2  13024  pwle2  13027  nnsf  13033  peano3nninf  13035  nninfex  13039  exmidsbthrlem  13051  sbthom  13055  isomninnlem  13059  trilpolemisumle  13065  trilpolemeq1  13067  trilpolemlt1  13068  sin24declemx24  13073  sin24declemsub  13075  sin24declemlt  13076
  Copyright terms: Public domain W3C validator