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

Theorem mp2an 410
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 408 . 2  |-  ( ps 
->  ch )
51, 4ax-mp 7 1  |-  ch
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 101
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 105
This theorem is referenced by:  mp4an  411  jaoi  646  mp3an  1243  barbara  2014  eqeq12i  2069  vtocl2  2626  spc2ev  2665  sbc2ie  2857  csbieb  2916  sseq12i  2999  uneq12i  3123  ineq12i  3164  nelpri  3427  ralpr  3453  rexpr  3454  preq12i  3480  dfop  3576  opeq12i  3582  breq12i  3801  mpteq2ia  3871  opex  3994  opi2  3998  opth2  4005  otth2  4006  opeqsn  4017  opeqpr  4018  uniop  4020  opelopaba  4031  braba  4032  opelopab  4036  brab  4037  opelopabaf  4038  unex  4204  snnex  4209  op1stb  4237  onun2i  4245  onsucssi  4260  ontr2exmid  4278  onsucsssucexmid  4280  onsucelsucexmid  4283  opthreg  4308  tfis  4334  finds  4351  finds2  4352  nnregexmid  4370  xpeq12i  4395  opelvv  4418  eqrelriiv  4462  eqrelrdv  4464  relsnop  4472  xpss  4474  xpex  4481  relop  4514  brco  4534  opelcnv  4545  brcnv  4546  asymref  4738  codir  4741  ssrnres  4791  dmprop  4823  op2ndb  4832  dfco2  4848  cossxp  4871  coex  4891  funsn  4976  fnsn  4981  feq23i  5069  resasplitss  5097  fabex  5106  fvex  5223  xpsn  5367  fmptap  5381  fvsn  5386  opabex  5413  acexmidlemv  5538  oveq12i  5552  oprabid  5565  oprabss  5618  caovcom  5686  opabex3  5777  iunex  5778  oprabex  5783  ofmres  5791  op1st  5801  op2nd  5802  fo1st  5812  fo2nd  5813  mpt2ex  5864  1stconst  5870  2ndconst  5871  algrflem  5878  dftpos4  5909  tpostpos  5910  tpossym  5922  frecex  6012  frecfnom  6017  sucinc  6056  fnoei  6063  oeiexg  6064  nnacli  6092  nnmcli  6093  elec  6176  ecovcom  6244  ecovass  6246  ecovdi  6248  entri  6297  endisj  6329  xpcomco  6331  phplem2  6347  ssfiexmid  6367  1lt2pi  6496  indpi  6498  1nq  6522  rec1nq  6551  1lt2nq  6562  ltaddnq  6563  halfnqq  6566  prarloclemarch2  6575  prarloclemlt  6649  prarloclemcalc  6658  genpelxp  6667  ltexprlempr  6764  recexprlempr  6788  cauappcvgprlemcl  6809  cauappcvgprlemladd  6814  caucvgprlemcl  6832  caucvgprprlemcl  6860  0r  6893  1sr  6894  m1r  6895  m1p1sr  6903  m1m1sr  6904  0lt1sr  6908  1ne0sr  6909  1idsr  6911  recexgt0sr  6916  prsradd  6928  caucvgsrlemoffres  6942  caucvgsr  6944  pitonnlem1p1  6980  pitonnlem2  6981  pitoregt0  6983  peano2nnnn  6987  axi2m1  7007  axprecex  7012  axcnre  7013  nnindnn  7025  nntopi  7026  0cn  7077  addcli  7089  mulcli  7090  mulcomi  7091  readdcli  7098  remulcli  7099  rexpssxrxp  7129  ltrelxr  7139  gtneii  7172  lttri3i  7174  letri3i  7175  ltnsymi  7176  lenlti  7177  ltlei  7178  mulgt0i  7186  mulgt0ii  7187  0lt1  7202  addcomi  7218  pncan3oi  7290  resubcli  7337  subcli  7350  pncan3i  7351  negsubi  7352  subnegi  7353  subeq0i  7354  neg11i  7355  negcon1i  7356  negcon2i  7357  mulneg1i  7473  mulneg2i  7474  mul2negi  7475  addgt0ii  7557  ltnegi  7559  lenegi  7560  ltnegcon2i  7561  lesub0i  7562  ltaddposi  7563  posdifi  7564  ltnegcon1i  7565  lenegcon1i  7566  subge0i  7567  1ap0  7655  ltapii  7698  recrecapi  7795  dividapi  7796  div0api  7797  rec11apii  7812  divdiv32api  7818  recgt0ii  7948  ltrecii  7959  ltdiv23ii  7968  nnssre  7994  nnind  8006  nnmulcli  8012  nnsubi  8029  0le2  8080  1lt3  8154  2lt4  8156  1lt4  8157  3lt5  8159  2lt5  8160  1lt5  8161  4lt6  8163  3lt6  8164  2lt6  8165  1lt6  8166  5lt7  8168  4lt7  8169  3lt7  8170  2lt7  8171  1lt7  8172  6lt8  8174  5lt8  8175  4lt8  8176  3lt8  8177  2lt8  8178  1lt8  8179  7lt9  8181  6lt9  8182  5lt9  8183  4lt9  8184  3lt9  8185  2lt9  8186  1lt9  8187  2muline0  8207  nn0addcli  8276  nn0mulcli  8277  nn0addge1i  8287  nn0addge2i  8288  dfz2  8371  halfnz  8394  9p1e10  8429  numnncl  8436  numltc  8452  le9lt10  8453  nummac  8471  8lt10  8558  7lt10  8559  6lt10  8560  5lt10  8561  4lt10  8562  3lt10  8563  2lt10  8564  1lt10  8565  eluzaddi  8595  eluzsubi  8596  eluz2nn  8607  uzuzle23  8609  eluzge3nn  8610  divfnzn  8653  elq  8654  qreccl  8674  xrltnr  8802  mnfltpnf  8807  xrex  8857  elicc2i  8909  ioomax  8918  iccmax  8919  ioopos  8920  elxrge0  8948  iccshftri  8964  iccshftli  8966  iccdili  8968  icccntri  8970  unitssre  8974  fz10  9012  fzpreddisj  9035  fldiv4p1lem1div2  9255  frecfzennn  9367  m1expcl2  9442  m1expcl  9443  nn0expcli  9446  sqmuli  9502  cu2  9517  i3  9520  subsqi  9528  binom2subi  9532  bcpasc  9634  4bc2eq6  9642  rei  9727  imi  9728  readdi  9756  imaddi  9757  remuli  9758  immuli  9759  cjaddi  9760  cjmuli  9761  ipcni  9762  crrei  9764  crimi  9765  rexfiuz  9816  sqrt1  9873  sqrt4  9874  sqrt9  9875  abs1  9899  sqrtmulii  9961  abslti  9965  abslei  9966  abssubi  9977  absmuli  9978  sqabsaddi  9979  sqabssubi  9980  abstrii  9982  climz  10044  abscn2  10066  recn2  10068  imcn2  10069  climabs  10071  climre  10073  climim  10074  3dvdsdec  10176  3dvds2dec  10177  odd2np1lem  10183  n2dvds1  10224  z4even  10228  ndvdsi  10245  flodddiv4  10246  sqr2irrlem  10250  ex-fl  10279  ex-ceil  10280  ex-bc  10282  ex-dvds  10283  bj-unex  10426  bj-nn0suc0  10462  bj-nntrans  10463  bj-nnelirr  10465
  Copyright terms: Public domain W3C validator