HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem adantl 388
Description: Inference adding a conjunct to the left of an antecedent.
Hypothesis
Ref Expression
adantl.1 |- (ph -> ps)
Assertion
Ref Expression
adantl |- ((ch /\ ph) -> ps)
Proof of Theorem adantl
StepHypRef Expression
1 adantl.1 . . 3 |- (ph -> ps)
21a1i 8 . 2 |- (ch -> (ph -> ps))
32imp 350 1 |- ((ch /\ ph) -> ps)
Colors of variables: wff set class
Syntax hints:   -> wi 3   /\ wa 223
This theorem is referenced by:  adantll 392  ad2antlr 405  ad2antrl 406  ad2antll 407  jaao 427  sylan9 468  mpan9 470  sylan9bb 538  im2anan9 561  im2anan9r 562  bi2bian9 632  pm5.18 658  pm5.75 747  ccase2 755  prlem1 768  3ad2ant3 800  ax11v2 1210  ax11b 1215  sbcom 1253  sbal1 1341  ax11eq 1356  ax11el 1357  ax11inda 1364  euim 1414  euor2 1430  2exeu 1439  2eu5 1446  eqeqan12d 1482  sylan9eq 1519  vtoclegft 1847  eqvinc 1874  reu3 1921  sbcthdv 1937  sbccomglem 1978  sbccomg 1979  sbcralt 1980  csbcomg 2007  hbcsb1gd 2017  hbcsbgd 2018  sylan9ss 2065  elin 2197  sspr 2466  unissel 2517  intab 2550  copsex4g 2784  opth1gOLD 2788  solin 2848  reuuni1 2872  alxfr 2886  ralxfrALT 2890  wefrc 2933  ordelon 2961  tz7.7 2963  ordunidif 2995  onint0 2997  onnmin 3005  onmindif 3050  onmindif2 3051  ordelsuc 3061  ordsucelsuc 3063  ordtri2or2 3068  ordsucun 3072  onsucuni2 3081  nlimsucg 3102  ordunisuc2 3105  limuni3 3113  tfi 3116  peano5 3143  findsg 3147  tfinds 3151  tfindsg 3152  ssnlim 3157  brinxp 3222  ideqg 3266  relssres 3376  relimasn 3409  soirri 3428  ssxprOLD 3461  ssxpr 3462  xpexr2 3466  unixp0 3504  funssres 3538  funun 3540  fununi 3549  resfunexg 3565  cofunexg 3566  fco 3621  funssxp 3623  fssres2 3629  f1o2 3678  f1orescnv 3689  fnbrfvb 3738  fvelimab 3750  ssimaex 3753  dmfco 3758  fvco 3759  fvopab3ig 3763  fvimacnv 3790  fvimacnvALT 3794  dff2 3802  fopabco 3817  fopabcos 3818  fconst5 3833  iunexg 3847  f1ocnvfv1 3863  f1ocnvfv2 3864  isotr 3882  isotrALT 3883  isoini 3885  f1oiso 3889  tfrlem11 3906  tfr3 3911  rdglim2 3934  eloprabg 3992  oprssoprval 4019  f2ndres 4078  curry1 4082  oe0lem 4136  oe0 4145  oev2 4146  oasuc 4147  omsuc 4149  oesuc 4150  oalim 4151  omlim 4152  oecl 4156  oawordri 4168  oaord1 4169  oaword2 4171  oawordeulem 4172  oaordex 4176  oa00 4177  oalimcl 4178  oaass 4179  oarec 4180  omord 4183  omwordi 4186  omwordri 4187  omword1 4188  om00 4190  omlimcl 4193  odi 4194  oewordi 4202  oewordri 4203  oelim2 4206  nnarcl 4216  oaabs 4236  nneob 4239  omsmo 4241  ecoprass 4304  ecoprdi 4305  elmapg 4317  elpm 4320  fundmen 4409  pw2en 4426  sbthlem8 4434  sdomdomtr 4449  ensdomtr 4451  domsdomtr 4456  enen2 4458  domen1 4459  domen2 4460  fodomr 4463  mapenlem2 4470  mapxpen 4475  xpmapenlem5 4480  phplem2 4489  phplem4 4491  php2 4494  php3 4495  onomeneq 4498  onfin 4499  pssnn 4513  ssfi 4515  isfinite2 4523  unfilem1 4524  unfilem3 4526  fodomfi 4540  iunfi 4543  pwfi 4545  suppr 4562  zfregfr 4573  inf3lem6 4590  dfom3 4602  r1ord3 4629  r1val1 4630  tz9.12lem1 4631  rankr1 4646  ranklim 4657  r1pwcl 4659  rankxplim 4684  rankxplim3 4686  rankxpsuc 4687  aceq3 4705  ac6lem 4726  kmlem9 4745  zorn2lem3 4762  zorn2lem4 4763  zorn2lem6 4765  zorn2lem7 4766  fodom 4770  fodomb 4772  brdom7disj 4776  brdom6disj 4777  unidom 4780  carden 4803  carddom 4808  sucdom 4814  unxpdomlem 4815  cardlim 4823  cardiun 4831  alephcard 4839  alephnbtwn 4840  alephnbtwn2 4841  alephord 4847  alephsucdom 4852  cardaleph 4857  alephsson 4866  alephfp 4872  alephval2 4874  cflim 4881  cfeq0 4886  axextnd 4915  axrepndlem1 4916  axrepndlem2 4917  axunnd 4920  axpowndlem2 4922  axpowndlem3 4923  axpowndlem4 4924  axpownd 4925  axregndlem2 4927  axregnd 4928  axinfndlem1 4929  axinfnd 4930  axacndlem4 4934  axacndlem5 4935  axacnd 4936  addasspi 4995  mulasspi 4997  distrpi 4998  addnidpi 5000  ltapi 5002  ltmpi 5003  ltaddpq 5051  ltexpq2 5053  halfpq 5054  ltbtwnpq 5056  prub 5070  genpnmax 5082  mulclprlem 5093  distrlem1pr 5099  distrlem2pr 5100  1idpr 5105  psslinpr 5107  prlem934b 5110  prlem934 5111  ltaddpr 5112  ltexprlem6 5119  ltexpri 5121  ltapr 5123  prlem936 5127  reclem3pr 5130  reclem4pr 5131  suplem2pr 5134  mulgt0sr 5186  suppsr3 5196  axcnre 5258  cnegextlem1 5317  cnegextlem3 5319  cnegext 5320  0cnALT 5322  subnegt 5366  subeq0t 5375  muladd11t 5394  negsubdit 5429  submul2t 5432  nncant 5441  addsub4t 5445  ltxrt 5467  ltxrltt 5472  letrt 5498  xrltnsymt 5523  xrlttrit 5525  xrlttrt 5526  xrletrt 5537  xrret 5542  xrre2t 5543  ltleaddt 5619  ltaddpost 5624  lenegcon2t 5632  subge0t 5647  recextlem1 5655  recext 5657  divdivdivt 5741  conjmult 5753  letrp1t 5772  lt2msq 5829  lerec2t 5837  lediv12it 5844  ledivp1t 5853  xrmax2 5858  xrmin1 5859  xrmin2 5860  peano2nn 5883  nn2get 5890  nnleltp1t 5901  nnaddm1clt 5905  halfaddsubt 5988  avglet 5991  sup2 5998  infm3 6001  infmsup 6015  xrsupsslem 6023  xrinfmsslem 6024  xrsupss 6025  xrinfmss 6026  xrub 6027  supxrre 6030  nn0addclt 6067  nn0ltp1let 6074  nn0ltlem1t 6076  elnnz1 6102  znegclt 6110  zltp1let 6128  zltlem1t 6131  gtndivt 6140  primet 6142  zeot 6146  zneo 6147  zneoOLD 6148  peano2uz2 6149  uzind 6153  uzindOLD 6156  uzwo4OLD 6158  flget 6178  ceilet 6193  qaddclt 6207  qmulclt 6209  qbtwnxr 6217  om2uzlt 6235  seq1rn2 6258  ser1recl 6268  ser1add 6276  shftval3t 6285  shftf 6288  2shft 6289  shftcan2t 6290  elioo3g 6317  elioc2t 6322  elico2t 6323  elicc2t 6324  ioossre 6328  uztrn 6360  eluzp1lt 6366  peano2uzr 6380  uzaddclt 6381  uzind4i 6386  uzwo 6387  uzwoOLD 6388  elfz2t 6404  eluzfzt 6409  elfzle3 6417  fznt 6425  fznn0sub2t 6431  fzaddelt 6432  fzsubelt 6433  fzoptht 6434  fzss2t 6436  fzelp1t 6440  elfzp1 6442  fzrevt 6443  fzrev2t 6444  fzrev2it 6445  fzrev3t 6446  fzneuzt 6450  fsequb 6455  fseqsupcl 6457  fseqsupub 6458  seqzeq 6487  seqzrn2 6488  expnnvalt 6504  expp1t 6506  expm1t 6515  expge0t 6522  expge1t 6524  mulexpt 6525  expaddt 6527  expword2it 6536  expmwordit 6537  exple1t 6538  sqlecant 6572  subsqt 6573  subsq2t 6574  bernneq 6583  expnbndt 6585  sqr11 6633  sqrmsq2 6636  sqr2irr 6659  crutOLD 6669  rimul 6675  replimt 6692  resubt 6741  imsubt 6744  cjsubt 6751  sqabsaddt 6783  sqabssubt 6784  absexpt 6803  seq1bnd 6847  seq1ublem 6848  cau3ir 6852  cvganz 6861  caubnd 6863  facnn2t 6876  facclt 6877  facdivt 6879  facwordit 6881  faclbnd 6882  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem3 6887  faclbnd4lem4 6888  faclbnd6 6891  facavgt 6892  bcval3t 6898  bcval4t 6899  bccl2t 6909  permnnt 6911  sumex 6919  sumeq2 6923  serzfsum 6942  fsum1 6943  fsum1s 6947  fsump1s 6951  fsumsplit 6958  csbfsum 6965  fsumcom 6966  fsumrev 6967  fsumconst 6976  fsumcmpndx2 6980  serzsplit 6994  binomlem1 7004  binomlem2 7005  binomlem4 7007  binomlem5 7008  binom1p 7011  bcxmas 7014  2climnn 7039  2climnn0 7040  climshft 7041  climshft2 7043  iserzshft2 7044  climrecl 7047  climge0 7049  climaddlem3 7052  climmullem1 7056  climmullem3 7058  climmullem4 7059  climmullem5 7060  climmullem8 7063  climsub 7066  iserzmulc1 7072  climcmplem 7073  climsqueeze 7076  climsqueeze2 7077  clim2serz 7081  climsup 7091  climcau 7092  caucvglem5 7097  caucvglem6 7098  caucvg 7099  ser1cmp2lem 7112  ser1cmp2 7113  isumnul 7138  isumreclt 7145  reccnv 7153  infcvglem3 7158  expcnvlem6 7167  geoisum1c 7180  cvgratlem1ALT 7182  cvgratlem1 7185  cvgratlem4 7188  cvgratlem5 7189  fsum0diaglem1 7191  fsum0diaglem2 7192  fsum0diag2 7194  fsum0diag4 7196  elcncf 7200  cncffvrn 7208  mulc1cncf 7214  ivthlem6 7221  ivthlem7 7222  ivthlem6OLD 7230  ivthlem7OLD 7231  eftclt 7245  efseq0ex 7253  efaddlem2 7281  efaddlem5 7284  efaddlem9 7288  efaddlem14 7293  efne0t 7311  efsubt 7313  efexpt 7314  reeftclt 7316  eftlclt 7321  reeftlclt 7322  abspef01tlub 7336  reeff1o 7368  sinsubt 7397  cossubt 7398  demoivre 7426  acdc3lem 7428  acdc2lem1 7430  acdc2lem2 7431  acdc5lem1 7433  acdc5lem2 7434  acdclem 7436  acdcALT 7438  nn0ennn 7439  xpnnen 7441  znnenlem 7443  znnenlemOLD 7444  znnen 7445  infpnlem1 7449  ruclem24 7476  ruclem27 7479  ruclem28 7480  infxpidmlem4 7498  infxpidmlem5 7499  infxpidmlem7 7501  infxpidmlem8 7502  infxpidmlem9 7503  infunabs 7508  infcdaabs 7509  infdif 7511  infdif2 7512  infmap2lem2 7522  alephadd 7524  iunopnt 7541  eltopss 7545  istps2 7549  eltgt 7560  eltg2t 7561  tg2t 7563  tgclt 7566  eltg3t 7568  tgss2t 7579  basgen2t 7581  sn0top 7589  iscld 7611  ntrval2 7628  ntrss 7630  elcls 7646  neiss2 7657  neiint 7660  isneip 7661  neips 7668  islp2 7688  clslp 7689  cnpco 7708  iscncl 7709  cnsscnp 7711  sncld 7726  metreslem 7762  metxp 7774  blval 7777  bl2in 7783  opni 7804  opni3 7806  blssopn 7807  blnei 7818  metcnplem 7825  metcnpi 7829  metcnpi2 7830  metcnpi3 7831  metcnpi4 7832  metcni2 7834  metcnss 7837  metcnss2 7838  metdnsconst 7840  cncfmet 7844  ioo2bl 7851  tgioolem 7853  tgioo 7854  lmconst 7872  lmnn 7873  iscau3 7876  iscau5 7878  caun0 7880  lmuni 7886  lmss 7888  lmfexlem2 7892  lmle 7895  metelcls 7900  xplmi 7907  xplm 7909  xpcn 7910  opr1cn 7912  bopcnlem2 7916  bopcnlem3 7917  fsumcnlem 7923  iscms2lem4 7926  lmcau 7930  cncms 7932  bcthlem2 7934  bcthlem7 7939  bcthlem9 7941  bcthlem14 7946  bcthlem16 7948  bcthlem18 7950  bcthlem20 7952  bcthlem21 7953  bcthlem26 7958  bcthlem28 7960  bcthlem31 7963  bcthlem33 7965  grpidinvlem2 7983  grpidinv 7986  grpideu 7987  grprcan 7997  grpinveu 7998  grpinvid1 8006  grpinvid2 8007  grplcan 8010  isgrp2i 8011  grpdivdiv 8022  grpmuldivass 8023  grppnpcan2 8027  grpnpncan 8029  abl4 8041  ablmuldiv 8044  abldivdiv4 8046  ablnnncan 8048  ablnnncan1 8050  subgopr 8055  subgabl 8060  vcdi 8108  vcdir 8109  vcass 8110  vcsubdir 8112  vcz 8126  nvex 8169  nvscom 8190  nvmdi 8210  nvsubadd 8215  cnnvm 8251  imsmetlem 8261  sqcn 8270  va1cnlem 8279  ipfval 8286  ipcl 8299  ip1cnilem6 8312  sspval 8316  sspmlem 8325  lnocoi 8352  nmoub3i 8368  0oo 8381  0lno 8382  nmlno0lem 8385  blocnilem 8395  cnph 8409  ipasslem1 8421  ipasslem2 8422  ipasslem4 8424  ipasslem5 8425  ipasslem11 8431  ipdi 8434  ipassr 8437  ipassr2 8438  ipsubdi 8440  ipblnfi 8447  ubthlem3 8462  ubthlem8 8467  ubthlem9 8468  ubthlem10 8469  minveclem17 8492  minveclem20 8495  minveclem22 8497  minveclem24 8499  minveclem25 8500  minveclem27 8502  minveclem30 8505  minveclem31 8506  htthlem5 8554  pilem2 8591  efif1lem5 8649  shftefif1olem 8661  shftefif1olemOLD 8662  eff1i 8665  axgroth3 8718  grothinf 8720  hvmul0ort 8815  hvaddsubvalt 8823  hvsub4t 8827  hvpncant 8829  hvmulcant 8860  hvmulcan2t 8861  hvaddsub4t 8866  normpyct 8934  hlimcaui 9027  helch 9037  hhssnv 9054  occont 9076  ocorth 9080  occllem6 9094  occl 9097  projlem2 9103  projlem8 9109  projlem26 9127  pjtheu 9150  pjeq2t 9156  shscl 9196  shsel1t 9200  hsupss 9224  spanss 9233  orthin 9285  chsscon2t 9340  chpsscon2t 9343  chdmm3t 9365  chdmm4t 9366  chdmj3t 9369  chdmj4t 9370  h1de2b 9392  h1de2bOLD 9393  spansnss2t 9415  spanunsn 9419  h1datom 9421  osumlem7 9501  nonbool 9513  5oalem1 9516  5oalem2 9517  5oalem3 9518  5oalem5 9520  pjot 9533  pjsumt 9572  pjoi0t 9579  pjnorm2t 9589  hosubnegt 9650  honegsubdit 9653  hosub4t 9656  unopf1ot 9756  unopnormt 9757  nmlnop0ALT 9835  lnopm 9840  lnophs 9841  lnopco 9843  lnopeq0 9847  nmopunt 9854  nmcopexlem3 9868  nmcopexlem6 9871  nmcoplb 9873  nmophm 9876  lnopcon 9878  lnfnsub 9890  nmbdfnlb 9893  nmcfnexlem3 9897  nmcfnexlem6 9900  nmcfnlb 9902  lnfncon 9905  nlelsh 9908  nlelch 9909  riesz3 9910  riesz4 9911  riesz1t 9913  cnlnadjlem2 9916  cnlnadjlem6 9920  adjbdlnb 9932  nmopco 9942  adjco 9947  rnbra 9953  bra11 9954  cnvbravalt 9956  cnvbramult 9960  kbass4t 9964  kbass5t 9965  leoprf2t 9972  leoprft 9973  leopmulit 9978  leopnmidt 9982  pjbdln 9987  hmopidmch 9990  hmopidmpj 9991  pjadjco 10000  pjss1co 10002  pjss2co 10003  pjorthco 10008  pjscj 10009  pjssdif2 10013  pjhmopidm 10020  pjinvar 10029  pjclem4a 10036  pjclem4 10037  pjadj2co 10042  pj3s 10045  pj3cor1 10047  hstoct 10059  hstnmoct 10060  hstoht 10069  stcltr1 10111  cvcon3t 10121  cvnbtwnt 10123  mdbr3 10134  mdbr4 10135  dmdmdt 10137  dmdbr3 10141  dmdbr4 10142  mdsl0 10145  ssmd2 10147  mdslmd1lem2 10161  mdslmd2 10165  mdslmd3 10167  mdslmd4 10168  atcveq0 10183  superpos 10189  chjatom 10192  chrelat 10199  cvbr3 10202  atcv0eq 10214  atoml 10217  atcvatlem 10220  irredlem3 10227  atcvat3 10231  atcvat4 10232  atmd 10234  mdsymlem3 10240  mdsymlem4 10241  mdsymlem5 10242  sumdmdi 10249  sumdmdlem 10252  sumdmdlem2 10253  dmdbr6at 10256  cdjreu 10264  cdj1 10265  cdj3lem1 10266  cdj3lem2b 10269  cdj3 10273  uninqs 10342  elo 10345  infi1 10347  fine 10348  sppfi 10376  cdrci 10381  oisbmj 10385  truni1 10386  cnrsfin 10396  cnrscoa 10397  mapdiscn 10398  cnvhmph 10414  hmphsyma 10415  hmphre 10417  hmphtr 10418  hmpher 10423  hmeogrp 10425  homcard 10426  qusp 10430  oefil2 10441  fgsb 10444  fgsb2 10449  cnfilca 10451  mslb1 10473  iintlem1 10476  iint 10478  1ded 10515  1cat 10536  cmpassoh 10573  homgrf 10574  ismonb 10580  ismonb1 10581  ismonb2 10582  imonclem 10583  ismonc 10584  cmpmon 10585  icmpmon 10587  idmon 10588
This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7
This theorem depends on definitions:  df-bi 147  df-an 225
Copyright terms: Public domain