ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantl Structured version   GIF version

Theorem adantl 262
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 261 . 2 ((φ χ) → ψ)
32ancoms 255 1 ((χ φ) → ψ)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem is referenced by:  sylan2  270  anim12ii  325  sylan9bb  438  ad2antrl  463  ad2antll  464  im2anan9  517  bi2bian9  528  jaao  626  ordi  717  con1bidc  756  con1bdc  760  dfandc  766  stabtestimpdc  812  dcor  829  annimdc  831  ccase2  859  rnlem  869  simpr1  896  simpr2  897  simpr3  898  3ad2ant3  913  simprl1  935  simprl2  936  simprl3  937  simprr1  938  simprr2  939  simprr3  940  simpr1l  947  simpr1r  948  simpr2l  949  simpr2r  950  simpr3l  951  simpr3r  952  simpr11  974  simpr12  975  simpr13  976  simpr21  977  simpr22  978  simpr23  979  simpr31  980  simpr32  981  simpr33  982  falimd  1241  xorbin  1256  xor2dc  1262  biassdc  1267  dfbi3dc  1269  xordidc  1271  ax11v2  1679  ax11b  1685  equs5or  1689  nfsbxyt  1797  sbcomxyyz  1824  2exeu  1970  dimatis  1995  gencbvex  2573  gencbval  2575  elrab3t  2670  euind  2701  reu6  2703  reuind  2717  sbcan  2778  sbcralt  2807  sbcrext  2808  csbcomg  2846  csbiebt  2859  sbcnestgf  2870  sseq1  2939  ddifnel  3048  elin  3099  undif3ss  3171  uneqdifeqim  3281  disjpr2  3404  diftpsn3  3475  preqr1g  3507  nfopd  3536  unissel  3579  trel  3831  iinexgm  3878  copsex2t  3952  sowlin  4027  ordelon  4065  suctr  4104  alxfr  4139  ralxfr  4144  rexxfr  4146  rabxfr  4148  reuhyp  4150  ordelsuc  4177  onsucelsucr  4179  onsucsssucr  4180  ordtriexmidlem  4188  onsucelsucexmidlem  4194  ordsucunielexmid  4196  regexmidlem1  4198  preleq  4213  eunex  4219  ordsuc  4221  nlimsucg  4222  onnmin  4224  tfi  4228  peano2  4241  opeliunxp  4318  posng  4335  sosng  4336  eqrelrdv2  4362  ideqg  4410  opeldmg  4463  relssres  4571  exse2  4622  brcodir  4635  xpidtr  4638  poltletr  4648  ssxpbm  4679  ssxp1  4680  ssxp2  4681  xpexr2m  4685  rnpropg  4723  elxp4  4731  elxp5  4732  dfco2a  4744  iota5  4810  iota2  4816  funssres  4864  funun  4866  fnsng  4869  fununi  4889  funimaexglem  4904  fneu  4925  fco  4977  fco2  4978  funssxp  4981  fssres2  4988  f1orescnv  5063  nffvd  5108  fnsnfv  5153  ssimaex  5155  funfvdm2  5158  dmfco  5162  fvco2  5163  fvmptss2  5168  respreima  5216  rexrn  5225  ralrn  5226  elrnrexdm  5227  ralrnmpt  5230  rexrnmpt  5231  ffvresb  5249  fcompt  5254  xpsng  5259  fprg  5267  fsnunres  5285  resfunexg  5303  funfvima3  5313  rexima  5315  ralima  5316  f1veqaeq  5329  f1ocnvfv1  5338  f1ocnvfv2  5339  fcofo  5345  foeqcnvco  5351  f1eqcocnv  5352  isoresbr  5370  isoini  5378  isoselem  5380  f1oiso  5386  riotabiia  5405  riota2f  5409  riota5f  5412  eloprabga  5510  ovmpt2x  5548  ovmpt2ga  5549  ovg  5558  oprssov  5561  caovcl  5574  caovimo  5613  f1opw2  5625  ofres  5644  resfunexgALT  5656  cofunexg  5657  iunexg  5665  offval3  5680  f2ndres  5706  elxp6  5715  releldm2  5730  oprabco  5757  1stconst  5761  2ndconst  5762  cnvf1o  5765  fo2ndf  5767  f1o2ndf1  5768  poxp  5771  mpt2xopoveq  5773  sprmpt2  5775  isprmpt2  5776  reldmtpos  5786  dftpos4  5796  tposf2  5801  iunon  5817  iordsmo  5830  tfrlem1  5841  tfrlemisucaccv  5856  tfrlemi1  5863  tfrexlem  5866  tfri3  5871  rdgivallem  5884  rdgon  5889  frec0g  5898  oasuc  5955  omsuc  5962  nnaass  5975  nndi  5976  nnsucelsuc  5981  nntri1  5985  nnaordi  5988  nnaword  5991  nnmord  5997  nnm00  6009  swoer  6041  eqer  6045  0er  6047  relelec  6053  ectocl  6080  iinerm  6085  eroveu  6104  ecopovtrn  6110  ecopover  6111  ecopovsymg  6112  ecopovtrng  6113  ecopoverg  6114  th3qlem1  6115  ecovass  6122  ecoviass  6123  ecovdi  6124  ecovidi  6125  ltpiord  6173  ltsopi  6174  mulclpi  6182  addasspig  6184  mulasspig  6186  distrpig  6187  addnidpig  6190  ltapig  6192  ltmpig  6193  nnppipi  6196  enqdc1  6215  addcmpblnq  6220  mulcmpblnq  6221  ordpipqqs  6227  addassnqg  6235  mulcanenq  6238  distrnqg  6240  mulidnq  6242  recmulnqg  6244  ltsonq  6251  ltanqg  6253  ltmnqg  6254  ltaddnq  6259  ltexnqq  6260  halfnqq  6261  ltbtwnnqq  6266  archnqq  6268  prarloclemarch  6269  prarloclemarch2  6270  ltrnqg  6271  enq0tr  6283  enq0er  6284  nqnq0  6290  addcmpblnq0  6292  mulcmpblnq0  6293  mulcanenq0ec  6294  nnnq0lem1  6295  mulnnnq0  6299  nqnq0a  6303  nqnq0m  6304  nq0m0r  6305  nq0a0  6306  distrnq0  6308  addassnq0  6311  nq02m  6313  prcdnql  6332  prcunqu  6333  prubl  6334  prloc  6339  prarloclemlt  6341  prarloclemlo  6342  prarloc  6351  genplt2i  6358  genprndl  6370  genprndu  6371  genpdisj  6372  genpassl  6373  genpassu  6374  addnqprllem  6376  addnqprulem  6377  addnqprl  6378  addnqpru  6379  addlocprlemeqgt  6381  nqprloc  6394  appdivnq  6401  prmuloc  6404  mulnqprl  6406  mulnqpru  6407  mullocprlem  6408  distrlem4prl  6417  distrlem4pru  6418  1idprl  6423  1idpru  6424  ltpopr  6426  ltsopr  6427  ltaddpr  6428  ltexprlemupu  6435  ltexprlemdisj  6437  ltexprlemloc  6438  ltexprlemfl  6440  ltexprlemrl  6441  ltexprlemfu  6442  ltexprlemru  6443  addcanprleml  6445  ltaprg  6449  recexprlemdisj  6458  recexprlemloc  6459  recexprlem1ssl  6461  recexprlem1ssu  6462  mulcmpblnrlemg  6481  ltsrprg  6488  mulasssrg  6499  distrsrg  6500  lttrsr  6503  ltposr  6504  ltsosr  6505  0idsr  6508  1idsr  6509  ltasrg  6511  recexsrlem  6514  mulgt0sr  6516  axmulass  6561  axdistr  6562  ax0id  6566  axcnre  6569  ltxrlt  6680  ltso  6690  muladd11  6733  readdcan  6740  cnegexlem1  6773  cnegexlem3  6775  cnegex  6776  addsubeq4  6813  subeq0  6823  renegcl  6858  mul2neg  6981  submul2  6982  ltleadd  7026  ltaddpos  7032  lt2sub  7040  le2sub  7041  lenegcon2  7047  cbvrald  7173  bdsepnft  7252  bj-om  7298  bj-nnen2lp  7315  strcollnft  7341  sscoll2  7345
  Copyright terms: Public domain W3C validator