Theorem adantrl 394

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 390	. 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 408  ad2ant2rl 411  anabss3 500  3ad2antr2 813  3ad2antr3 814  sbcom 1258  ifboth 2375  ordelord 2970  ordsucun 3082  foco 3682  isocnv 3896  tfrlem9 3919  tfrlem11 3921  oaass 4195  omordi 4197  omwordri 4203  odi 4210  oewordri 4219  dom2d 4404  fundmen 4428  sbthlem9 4455  mapenlem2 4490  mapunen 4502  ssenen 4504  unifiOLD 4557  supmo 4576  inf3lem6 4618  axacndlem4 4962  axacndlem5 4963  axacnd 4964  ltapq 5076  ltmpq 5077  ltexpq 5080  prlem936a 5153  ssgt0sr 5217  cnegextlem2 5346  muladdt 5421  xrret 5569  rec11rt 5779  divdivdivt 5785  divdiv23t 5792  ltmul12it 5841  lemul12ait 5842  lemul12itOLD 5843  ltdiv23t 5892  lediv23t 5893  zextltt 6190  zmax 6220  qbtwnre 6278  2shft 6352  icounlem 6412  ioojoint 6416  fznn0subt 6498  fzaddelt 6500  fzsubelt 6501  fsequb 6523  expsubt 6598  expordit 6600  sqlecant 6641  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 7489  acdc5lem2 7492  infpnlem1 7506  infxpidmlem7 7558  infxpidmlem11 7562  istps2 7607  tgss2t 7637  2basgent 7641  clsval2 7685  metcnp 7887  lmbr 7928  causs 7955  metelcls 7965  xplmi 7973  xpcn 7976  cmsss 7997  bcthlem18 8016  bcthlem21 8019  bcthlem24 8022  bcthlem25 8023  grplcan 8075  nvmfval 8264  nvmf 8266  nvsubadd 8275  nvlmle 8333  sqcn 8335  sspmval 8392  sspival 8397  lnoadd 8419  lnomul 8421  nvcnpi3 8422  nvcnpi4 8423  nmosetre 8427  0lno 8450  sspph 8515  ubthlem12 8540  ubthlem13 8541  ubthlem14 8542  minveclem30 8574  htthlem6 8625  htthlem9 8628  hiassdit 8957  chocuni 9172  shscl 9281  fh1t 9561  fh2t 9562  cm2jt 9563  spansncv 9597  5oalem2 9600  adjsymt 9759  nmopsetretALT 9790  nmfnsetret 9804  cnvadj 9816  cnvunopt 9842  unoplint 9844  hmoplint 9866  lnopm 9925  hmopst 9945  hmopmt 9946  hmopcot 9948  adjlnopt 10019  adjmult 10025  adjaddt 10026  mdsl0 10237  ssmd2 10239  mdexch 10262  superpos 10281  chrelat2 10292  atcvatlem 10312  atcvat 10313  irredlem1 10317  irred 10321  atcvat3 10323  atcvat4 10324  mdsymlem3 10332  mdsymlem5 10334  cdj3lem2b 10364  ghomf1olem 10396

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