Theorem adantrl 403

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

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

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 380	. . 3 |- (ph -> (ps -> ch))
3	2	adantld 399	. 2 |- (ph -> ((th /\ ps) -> ch))
4	3	imp 357	1 |- ((ph /\ (th /\ ps)) -> ch)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  ad2ant2l 417  ad2ant2rl 420  anabss3 511  3ad2antr2 825  3ad2antr3 826  sbcom 1300  ifboth 2427  ordelord 3027  ordsucun 3139  foco 3739  isocnv 3954  tfrlem9 3977  tfrlem11 3979  oaass 4253  omordi 4255  omwordri 4261  odi 4268  oewordri 4277  dom2d 4465  fundmen 4489  sbthlem9 4518  mapenlem2 4555  mapunen 4567  ssenen 4569  unifi 4618  supmo 4636  inf3lem6 4680  axacndlem4 5027  axacndlem5 5028  axacnd 5029  ltapq 5141  ltmpq 5142  ltexpq 5145  prlem936a 5218  ssgt0sr 5282  cnegexlem2 5411  muladd 5486  xrre 5634  rec11r 5837  divdivdiv 5843  divdiv23 5850  ltmul12a 5899  lemul12b 5900  lemul12aOLD 5901  ltdiv23 5952  lediv23 5953  zextlt 6275  zmax 6305  qbtwnre 6331  modadd1 6380  iooshf 6421  icounlem 6438  ioojoin 6442  fznn0sub 6524  fzaddel 6526  fzsubel 6527  fsequb 6549  2shfti 6611  expsub 6687  expordi 6689  sqlecan 6730  cau3iri 7005  facndiv 7033  bccl2 7061  fsumcllem 7104  fsumcom 7118  fsumshf 7121  fsummulc1 7123  serzcmp0 7145  climaddlem1 7204  climaddc1 7208  climaddc2 7209  climmullem3 7212  climmullem5 7214  climmullem6 7215  climsubc2 7221  climcmpc1 7229  climcaui 7246  caucvglem6 7252  caucvgi 7253  serzf0i 7259  ser1f0i 7260  ser1cmp2i 7267  cvgratlem1 7340  mulc1cncf 7369  acdc2lem2 7581  acdc5lem2 7584  infpnlem1 7598  infxpidmlem7 7650  infxpidmlem11 7654  istps2 7698  tgss2 7726  2basgen 7730  clsval2 7770  metcnp 7972  lmbr 8013  causs 8040  metelcls 8050  xplmi 8058  xpcn 8061  cmsss 8082  bcthlem18 8101  bcthlem21 8104  bcthlem24 8107  bcthlem25 8108  grplcan 8159  nvmfval 8348  nvmf 8350  nvsubadd 8359  nvlmle 8417  sqcn 8419  sspmval 8476  sspival 8481  lnoadd 8503  lnomul 8505  nvcnpi3 8506  nvcnpi4 8507  nmosetre 8511  0lno 8534  sspph 8599  ubthlem12 8624  ubthlem13 8625  ubthlem14 8626  minveclem30 8658  htthlem6 8709  htthlem9 8712  hiassdi 9040  chocunii 9255  shscli 9364  fh1 9644  fh2 9645  cm2j 9646  spansncvi 9680  5oalem2 9683  adjsym 9842  nmopsetretALT 9873  nmfnsetre 9887  cnvadj 9899  cnvunop 9925  unoplin 9927  hmoplin 9949  lnopmi 10008  hmops 10028  hmopm 10029  hmopco 10031  adjlnop 10102  adjmul 10108  adjadd 10109  mdsl0 10321  ssmd2 10323  mdexchi 10346  superpos 10365  chrelat2i 10376  atcvatlem 10396  atcvati 10397  irredlem1 10401  irredi 10405  atcvat3i 10407  atcvat4i 10408  mdsymlem3 10416  mdsymlem5 10418  cdj3lem2b 10448  ghomf1olem 10481

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 154  df-an 232

Copyright terms: Public domain