NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  mp2an Unicode version

Theorem mp2an 653
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 651 . 2
51, 4ax-mp 5 1
Colors of variables: wff setvar class
Syntax hints:   wi 4   wa 358
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360
This theorem is referenced by:  mp4an  654  mp3an  1277  nanbi12i  1300  cadtru  1401  spim  1975  barbara  2301  eqeq12i  2366  vtocl2  2910  spc2ev  2947  mosub  3014  sbc2ie  3113  csbieb  3174  nineq12i  3239  symdifeq12i  3253  sseq12i  3297  uneq12i  3416  ineq12i  3455  keephyp  3716  nelpri  3754  ralpr  3779  rexpr  3780  preq12i  3804  opkeq12i  4064  ninex  4098  inex  4105  unex  4106  difex  4107  symdifex  4108  pw111  4170  xpkeq12i  4203  eqrelkriiv  4213  eqrelkrdv  4214  opkelopkab  4246  opkelxpk  4248  opkelcnvk  4250  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelcok  4262  opksnelsik  4265  sikss1c1c  4267  elssetk  4270  opkelimagek  4272  ins2kss  4279  ins3kss  4280  cokrelk  4284  cnvkexg  4286  xpkex  4289  ssetkex  4294  sikexlem  4295  imakex  4300  dfpw12  4301  insklem  4304  cokex  4310  dfidk2  4313  addceq12i  4388  addcex  4394  dfnnc2  4395  nnc0suc  4412  nncaddccl  4419  0fin  4423  nnsucelrlem1  4424  nnsucelr  4428  nndisjeq  4429  ltfinp1  4462  lefinlteq  4463  lefinrflx  4467  ssfin  4470  eqpwrelk  4478  ncfinraise  4481  ncfinlower  4483  eqtfinrelk  4486  tfin0c  4497  tfin1c  4499  tfinltfinlem1  4500  tfinltfin  4501  oddfinex  4504  0ceven  4505  evenodddisjlem1  4515  nnpweq  4523  srelk  4524  sfin01  4528  sfinltfin  4535  vfinspsslem1  4550  dfphi2  4569  opex  4588  breq12i  4648  opelopaba  4703  braba  4704  opelopab  4708  brab  4709  opelopabaf  4710  setconslem1  4731  dfsset2  4743  imaex  4747  coex  4750  dfsi2  4751  brsset  4758  xpeq12i  4806  dmprop  5070  xpex  5115  resex  5117  feq23i  5219  fvi  5442  swapres  5512  opfv1st  5514  opfv2nd  5515  oveq12i  5535  caovcom  5625  mpteq2ia  5659  txpex  5785  brcup  5815  composefn  5818  brdisj  5822  braddcfn  5826  pprodex  5838  brcross  5849  brpw1fn  5854  fnfullfun  5858  dfnnc3  5885  qsex  5983  mapval  6011  endisj  6051  xpassen  6057  ensn  6058  enmap2lem1  6063  enmap1lem1  6069  enpw1pw  6075  enpw  6087  brlec  6113  mucnc  6131  1cnc  6139  ncspw1eu  6159  tc0c  6163  tcdi  6164  tc1c  6165  tc2c  6166  ce0nnul  6177  ce0addcnnul  6179  ce0nn  6180  cenc  6181  fce  6188  ce2  6192  lecncvg  6199  nclenc  6222  taddc  6229  letc  6231  ce0t  6232  cet  6234  ce0lenc1  6239  brtcfn  6246  ncvsq  6256  nnltp1c  6262  nmembers1lem2  6269  nncdiv3  6277  nnc3n3p1  6278  nchoicelem9  6297  nchoicelem14  6302  nchoicelem17  6305  fnfreclem2  6318  fnfreclem3  6319
  Copyright terms: Public domain W3C validator