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

Theorem adantl 452
Description: Inference adding a conjunct to the left of an antecedent. (Contributed by NM, 30-Aug-1993.) (Proof shortened by Wolf Lammen, 23-Nov-2012.)
Hypothesis
Ref Expression
adantl.1 (φψ)
Assertion
Ref Expression
adantl ((χ φ) → ψ)

Proof of Theorem adantl
StepHypRef Expression
1 adantl.1 . . 3 (φψ)
21adantr 451 . 2 ((φ χ) → ψ)
32ancoms 439 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:  sylan2  460  jaao  495  anim12ii  553  sylan9bb  680  ad2antrl  708  ad2antll  709  im2anan9  808  bi2bian9  845  pm5.54  870  ccase2  914  rnlem  931  simpr1  961  simpr2  962  simpr3  963  3ad2ant3  978  simprl1  1000  simprl2  1001  simprl3  1002  simprr1  1003  simprr2  1004  simprr3  1005  simpr1l  1012  simpr1r  1013  simpr2l  1014  simpr2r  1015  simpr3l  1016  simpr3r  1017  simpr11  1039  simpr12  1040  simpr13  1041  simpr21  1042  simpr22  1043  simpr23  1044  simpr31  1045  simpr32  1046  simpr33  1047  falimd  1329  nfimdOLD  1809  spimt  1974  ax11v2  1992  ax11b  1995  nfsb4t  2080  sbcom  2089  sbal1  2126  ax11eq  2193  ax11el  2194  ax11inda  2200  ax11v2-o  2201  2eu5  2288  dimatis  2320  nfrald  2665  nfreud  2783  nfrmod  2784  nfrmo  2786  nfrab  2792  gencbvex  2901  euind  3023  reu6  3025  reuind  3039  sbcan  3088  sbcralt  3118  sbcrext  3119  csbcomg  3159  csbiebt  3172  sbcnestgf  3183  sseq1  3292  undif3  3515  uneqdifeq  3638  ifeq1da  3687  ifeq2da  3688  ifclda  3689  ifbothda  3692  diftpsn3  3849  unissel  3920  unissint  3950  uniintsn  3963  pwadjoin  4119  opkelopkabg  4245  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  dfpw12  4301  pw1equn  4331  pw1eqadj  4332  nfiotad  4342  iota5  4359  iota2  4367  eladdc  4398  peano2  4403  nndisjeq  4429  nnceleq  4430  lefinaddc  4450  prepeano4  4451  preaddccan2  4455  ltfinirr  4457  ltfintr  4459  lefinlteq  4463  ltfintri  4466  ltlefin  4468  ssfin  4470  ncfinsn  4476  tfinprop  4489  tfinnnul  4490  tfin11  4493  tfindi  4496  tfinltfinlem1  4500  evenodddisj  4516  nnadjoin  4520  nnpweq  4523  sfintfin  4532  sfinltfin  4535  sfin111  4536  vfinspnn  4541  vfinspclt  4552  vinf  4555  nulnnn  4556  nfopd  4605  copsex2t  4608  opeliunxp  4820  ideqg  4868  ideqg2  4869  ssxpb  5055  xpcan  5057  xpcan2  5058  dfco2a  5081  xpexr2  5110  dfxp2  5113  funeu  5131  funssres  5144  fununi  5160  fnbr  5185  fco  5231  funssxp  5233  fssres2  5239  f1orescnv  5301  nffvd  5335  eqfnfv  5392  funfvbrb  5401  respreima  5410  fnasrn  5417  dff3  5420  ffvresb  5431  fconst5  5455  f1ocnvfv1  5476  isotr  5495  f1oiso  5499  funsi  5520  eloprabga  5578  ovg  5601  oprssov  5603  caovcl  5623  fvmpti  5699  fvmptss  5705  brtxp  5783  composevalg  5817  fnpprod  5843  fvfullfunlem3  5863  clos1conn  5879  po0  5939  erdisj  5972  ectocl  5992  xpsnen2g  6054  enadj  6060  enmap2lem3  6065  enmap2lem5  6067  enmap1lem5  6073  enprmaplem5  6080  nenpw1pwlem2  6085  eqncg  6126  ncdisjun  6136  1cnc  6139  ncssfin  6151  pw1eltc  6162  tcdi  6164  ce0nnul  6177  ce0nnuli  6178  cenc  6181  ce0  6190  lecidg  6196  lec0cg  6198  lecncvg  6199  addlec  6208  lecponc  6213  leconnnc  6218  addceq0  6219  dflec3  6221  ce2le  6233  cet  6234  nclenn  6249  addcdi  6250  muc0or  6252  addccan2nclem1  6263  ncslesuc  6267  nnc3n3p1  6278  spacind  6287  spacis  6288  nchoicelem8  6296  nchoicelem9  6297  nchoicelem12  6300  nchoicelem17  6305  frecxp  6314  fnfreclem3  6319  fnfrec  6320
  Copyright terms: Public domain W3C validator