Theorem adantrl 396

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 373	. . 3 |- (ph -> (ps -> ch))
3	2	adantld 392	. 2 |- (ph -> ((th /\ ps) -> ch))
4	3	imp 350	1 |- ((ph /\ (th /\ ps)) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2l 410  ad2ant2rl 413  anabss3 502  3ad2antr2 815  3ad2antr3 816  sbcom 1260  ifboth 2379  ordelord 2976  ordsucun 3088  foco 3688  isocnv 3902  tfrlem9 3925  tfrlem11 3927  oaass 4201  omordi 4203  omwordri 4209  odi 4216  oewordri 4225  dom2d 4410  fundmen 4434  sbthlem9 4461  mapenlem2 4496  mapunen 4508  ssenen 4510  unifiOLD 4570  supmo 4585  inf3lem6 4627  axacndlem4 4974  axacndlem5 4975  axacnd 4976  ltapq 5088  ltmpq 5089  ltexpq 5092  prlem936a 5165  ssgt0sr 5229  cnegextlem2 5358  muladdt 5433  xrret 5581  rec11rt 5781  divdivdivt 5787  divdiv23t 5794  ltmul12it 5843  lemul12ait 5844  lemul12itOLD 5845  ltdiv23t 5894  lediv23t 5895  zextltt 6192  zmax 6222  qbtwnre 6279  2shft 6353  icounlem 6413  ioojoint 6417  fznn0subt 6499  fzaddelt 6501  fzsubelt 6502  fsequb 6524  expsubt 6599  expordit 6601  sqlecant 6642  cau3ir 6915  facndivt 6943  bccl2t 6971  fsumcllem 7014  fsumcom 7028  fsumshft 7031  fsummulc1 7033  serzcmp0 7055  climaddlem1 7114  climaddc1 7118  climaddc2 7119  climmullem3 7122  climmullem5 7124  climmullem6 7125  climsubc2 7131  climcmpc1 7139  climcau 7156  caucvglem6 7162  caucvg 7163  serzf0 7169  ser1f0 7170  ser1cmp2 7177  cvgratlem1 7250  mulc1cncf 7279  acdc2lem2 7490  acdc5lem2 7493  infpnlem1 7507  infxpidmlem7 7559  infxpidmlem11 7563  istps2 7608  tgss2t 7636  2basgent 7640  clsval2 7682  metcnp 7884  lmbr 7925  causs 7952  metelcls 7962  xplmi 7970  xpcn 7973  cmsss 7994  bcthlem18 8013  bcthlem21 8016  bcthlem24 8019  bcthlem25 8020  grplcan 8071  nvmfval 8260  nvmf 8262  nvsubadd 8271  nvlmle 8329  sqcn 8331  sspmval 8388  sspival 8393  lnoadd 8415  lnomul 8417  nvcnpi3 8418  nvcnpi4 8419  nmosetre 8423  0lno 8446  sspph 8511  ubthlem12 8536  ubthlem13 8537  ubthlem14 8538  minveclem30 8570  htthlem6 8621  htthlem9 8624  hiassdit 8952  chocuni 9167  shscl 9276  fh1t 9556  fh2t 9557  cm2jt 9558  spansncv 9592  5oalem2 9595  adjsymt 9754  nmopsetretALT 9785  nmfnsetret 9799  cnvadj 9811  cnvunopt 9837  unoplint 9839  hmoplint 9861  lnopm 9920  hmopst 9940  hmopmt 9941  hmopcot 9943  adjlnopt 10014  adjmult 10020  adjaddt 10021  mdsl0 10232  ssmd2 10234  mdexch 10257  superpos 10276  chrelat2 10287  atcvatlem 10307  atcvat 10308  irredlem1 10312  irred 10316  atcvat3 10318  atcvat4 10319  mdsymlem3 10327  mdsymlem5 10329  cdj3lem2b 10359  ghomf1olem 10391

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