Theorem ad2antlr 407

Description: Deduction adding conjuncts to antecedent.

Hypothesis

Ref	Expression
ad2ant.1	|- (ph -> ps)

Assertion

Ref	Expression
ad2antlr	|- (((ch /\ ph) /\ th) -> ps)

Proof of Theorem ad2antlr

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 |- (ph -> ps)
2	1	adantl 390	. 2 |- ((ch /\ ph) -> ps)
3	2	adantr 391	1 |- (((ch /\ ph) /\ th) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simplr 415  ax11eq 1365  ax11el 1366  tfindsg 3169  caoprord3 4065  oesuc 4173  oelim 4176  oaordi 4187  oaass 4202  odi 4217  omass 4218  oen0 4220  oelim2 4229  undom 4445  xpdom2 4449  mapenlem1 4496  mapenlem2 4497  php3 4522  php3OLD 4523  fiint 4576  fiintOLD 4577  suppr 4606  fodom 4815  unxpdomlem 4861  npex 5110  elnp 5111  cnegext 5367  divdivdivt 5794  lemul12it 5853  lt2mul2divt 5881  lediv12it 5905  lediv2it 5906  xrmax2 5919  xrsupsslem 6085  xrinfmsslem 6086  xrub 6089  supxrre 6092  supxrun 6094  supxrunb1 6098  supxrunb2 6099  supxrbnd 6100  monoord 6302  elioc2t 6398  elico2t 6399  elicc2t 6400  elfzp1 6518  fsequb 6531  sqr11 6711  absmaxt 6904  seq1bnd 6917  cvganz 6931  caubnd 6933  facndivt 6950  faclbnd 6952  sumeq2 6992  fsumcmpndx2 7049  2climnn 7109  2climnn0 7110  climrecl 7117  climsqueeze 7147  climsqueeze2 7148  climsup 7162  climcau 7163  caucvglem6 7169  caucvg 7170  reccnv 7225  cvgratlem2 7258  cvgratlem3 7259  fsum0diaglem2 7264  fsum0diag4 7268  acdc3lem 7494  acdc2lem2 7497  acdc5lem2 7500  acdclem 7502  infxpidmlem12 7571  basgen2t 7645  fctopOLD 7654  elcls3 7715  islp2 7751  iscnp2 7765  cnpco 7773  blss 7857  metcnplem 7890  metcnp 7891  metcni2 7899  metcnp3 7900  metcnss2 7903  tgioolem 7918  lmnn 7939  metcnp4lem2 7973  metcn4 7975  xpcn 7980  bcthlem2 8004  bcthlem13 8015  bcthlem14 8016  bcthlem27 8029  bcthlem28 8030  grpidinv 8056  grpideu 8057  isgrp2i 8079  nvmul0or 8275  sm1cnilem 8350  sspval 8385  nmoub3i 8439  nmo0 8454  blocnilem 8467  blocni 8468  ipblnfi 8519  ubthlem3 8534  ubthlem5 8536  ubthlem13 8544  minveclem27 8574  minveclem31 8578  hvmul0ort 8896  hvaddsub4t 8947  occont 9162  ocorth 9166  occllem6 9180  projlem25 9212  osumlem4 9583  5oalem1 9601  5oalem2 9602  3oalem2 9610  pjds3 9660  nmopub2tALT 9835  nmfnleub2t 9852  hmopadj2t 9867  lnopcon 9965  lnfncon 9992  nlelch 9996  cnlnadjlem6 10007  kbass5t 10055  leopnmidt 10073  nmopleidt 10074  hmopidmch 10081  pjss2co 10094  pjssdif1 10105  pj3cor1 10140  mdsl0 10240  mdslmd1lem1 10255  mdslmd1lem2 10256  csmdsym 10264  superpos 10284  atoml 10312  irredlem2 10321  irredlem3 10322  atcvat3 10326  atcvat4 10327  mdsymlem5 10337  cdjreu 10362  cdj1 10363  cdrci 10488  cnrsfin 10503  cnrscoa 10504  mapdiscn 10505  sfvlim 10584  iintlem1 10611  trnij 10616  cmpasso 10685

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