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

Theorem adantr 451
Description: Inference adding a conjunct to the right of an antecedent. (Contributed by NM, 30-Aug-1993.)
Hypothesis
Ref Expression
adantr.1
Assertion
Ref Expression
adantr

Proof of Theorem adantr
StepHypRef Expression
1 adantr.1 . . 3
21a1d 22 . 2
32imp 418 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:  adantl  452  jaao  495  anim12ii  553  sylan9bb  680  ad2antrr  706  ad2antlr  707  ad2antrl  708  ad3antrrr  710  ad3antlr  711  ad4antr  712  ad4antlr  713  ad5antr  714  ad5antlr  715  ad6antr  716  ad6antlr  717  ad7antr  718  ad7antlr  719  ad8antr  720  ad8antlr  721  ad9antr  722  ad9antlr  723  ad10antr  724  ad10antlr  725  simp-4l  742  simp-4r  743  simp-5l  744  simp-5r  745  simp-6l  746  simp-6r  747  simp-7l  748  simp-7r  749  simp-8l  750  simp-8r  751  simp-9l  752  simp-9r  753  simp-10l  754  simp-10r  755  simp-11l  756  simp-11r  757  im2anan9  808  bi2bian9  845  ccase2  914  simpl1  958  simpl2  959  simpl3  960  3ad2ant1  976  3ad2ant2  977  simpll1  994  simpll2  995  simpll3  996  simplr1  997  simplr2  998  simplr3  999  simpl1l  1006  simpl1r  1007  simpl2l  1008  simpl2r  1009  simpl3l  1010  simpl3r  1011  simpl11  1030  simpl12  1031  simpl13  1032  simpl21  1033  simpl22  1034  simpl23  1035  simpl31  1036  simpl32  1037  simpl33  1038  cad1  1398  nfimdOLD  1809  ax12  1935  spimt  1974  sbequi  2059  nfsb4t  2080  dvelimdf  2082  sbcom  2089  ax12from12o  2156  ax11eq  2193  ax11el  2194  ax11indalem  2197  nfeud  2218  nfmod  2219  euan  2261  datisi  2313  fresison  2321  nfabd  2508  ralbid  2632  rexbid  2633  nfrald  2665  ralimdv  2693  ralcom2  2775  nfreud  2783  nfrmod  2784  reubidv  2795  rmobidv  2800  rabbidv  2851  elex22  2870  gencbvex  2901  rspct  2948  ceqsrexbv  2973  elrabf  2993  eueq3  3011  reu6  3025  reuind  3039  sbc2or  3054  sbcrext  3119  csbexg  3146  csbcomg  3159  csbiebt  3172  csbnestgOLD  3187  csbnest1gOLD  3189  sbcco3gOLD  3192  csbco3gOLD  3194  elin  3219  sseq1  3292  undif3  3515  difrab  3529  uneqdifeq  3638  diftpsn3  3849  eluni  3894  dfnfc2  3909  iuneq12d  3993  iuneq2d  3994  pwadjoin  4119  opkth1g  4130  elxpk  4196  opkabssvvk  4208  opkelopkabg  4245  opkelcokg  4261  opkelimagekg  4271  pw1equn  4331  pw1eqadj  4332  nfiotad  4342  findsd  4410  finds  4411  nnsucelr  4428  nndisjeq  4429  nnceleq  4430  nulge  4456  leltfintr  4458  ltfinp1  4462  lefinlteq  4463  ltfintri  4466  lenltfin  4469  ssfin  4470  ncfinsn  4476  ncfineleq  4477  ncfinraise  4481  ncfinlower  4483  tfin11  4493  tfinsuc  4498  tfinltfinlem1  4500  tfinltfin  4501  evennn  4506  oddnn  4507  sucevenodd  4510  sucoddeven  4511  evenodddisj  4516  nnadjoin  4520  sfindbl  4530  sfintfin  4532  sfinltfin  4535  sfin111  4536  vfinspnn  4541  vfintle  4546  vfinspsslem1  4550  vfinspss  4551  vinf  4555  phi11lem1  4595  nfopd  4605  copsexg  4607  elopab  4696  opeliunxp2  4822  ideqg  4868  brres  4949  dminss  5041  ssxpb  5055  xpcan  5057  xpcan2  5058  elxp4  5108  xpexr2  5110  funeu  5131  fununi  5160  funfni  5183  fco  5231  funssxp  5233  feu  5242  fimacnvdisj  5244  f1ss  5262  f1ores  5300  f1imacnv  5302  foimacnv  5303  fun11iun  5305  f1o00  5317  nffvd  5335  tz6.12-1  5344  fvelimab  5370  fvun  5378  eqfnfv  5392  fvimacnv  5403  ffvelrn  5415  dff3  5420  dffo3  5422  dffo4  5423  funiunfv  5467  f1ocnvfv1  5476  f1ofveu  5480  isocnv  5491  isotr  5495  isoini  5497  isoini2  5498  funsi  5520  oprabid  5550  eloprabga  5578  ov6g  5600  oprssov  5603  caovord3  5631  mpteq2dv  5668  cbvmpt2x  5678  fmpt2x  5730  composevalg  5817  fnpprod  5843  fnfullfunlem1  5856  clos10  5887  weds  5938  po0  5939  ersymb  5953  ertr  5954  erref  5959  erth  5968  qsdisj  5995  enadj  6060  enmap2lem3  6065  enprmaplem3  6078  nenpw1pwlem2  6085  brltc  6114  eqncg  6126  ncdisjun  6136  peano4nc  6150  eqtc  6161  pw1eltc  6162  tcdi  6164  ce0nnuli  6178  cenc  6181  lecidg  6196  lec0cg  6198  lecncvg  6199  sbthlem1  6203  sbthlem3  6205  leconnnc  6218  addceq0  6219  taddc  6229  tlecg  6230  ce2le  6233  cet  6234  nclenn  6249  addcdi  6250  muc0or  6252  lemuc1  6253  addccan2nc  6265  nmembers1lem3  6270  nmembers1  6271  nnc3n3p1  6278  spacind  6287  nchoicelem3  6291  nchoicelem4  6292  nchoicelem6  6294  nchoicelem7  6295  nchoicelem8  6296  nchoicelem9  6297  nchoicelem12  6300  nchoicelem14  6302  nchoicelem15  6303  nchoicelem17  6305  frecxp  6314  dmfrec  6316  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator