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 812  3ad2antr3 813  sbcom 1256  ifboth 2371  ordelord 2965  ordsucun 3077  foco 3673  isocnv 3887  tfrlem9 3910  tfrlem11 3912  oaass 4185  omordi 4187  omwordri 4193  odi 4200  oewordri 4209  dom2d 4391  fundmen 4415  sbthlem9 4441  mapenlem2 4476  mapunen 4488  ssenen 4490  unifi 4538  supmo 4556  inf3lem6 4598  axacndlem4 4942  axacndlem5 4943  axacnd 4944  ltapq 5056  ltmpq 5057  ltexpq 5060  prlem936a 5133  ssgt0sr 5197  cnegextlem2 5326  muladdt 5401  xrret 5550  rec11rt 5743  divdivdivt 5749  divdiv23t 5756  ltmul12it 5805  lemul12ait 5806  lemul12itOLD 5807  ltdiv23t 5848  lediv23t 5849  zextltt 6145  zmax 6176  qbtwnre 6224  2shft 6297  icounlem 6353  fznn0subt 6438  fzaddelt 6440  fzsubelt 6441  fsequb 6463  expsubt 6537  expordit 6539  sqlecant 6580  cau3ir 6860  facndivt 6888  bccl2t 6917  fsumcllem 6960  fsumcom 6974  fsumshft 6977  fsummulc1 6979  serzcmp0 7001  climaddlem1 7058  climaddc1 7062  climaddc2 7063  climmullem3 7066  climmullem5 7068  climmullem6 7069  climsubc2 7075  climcmpc1 7083  climcau 7100  caucvglem6 7106  caucvg 7107  serzf0 7113  ser1f0 7114  ser1cmp2 7121  cvgratlem1 7193  mulc1cncf 7222  acdc2lem2 7439  acdc5lem2 7442  infpnlem1 7457  infxpidmlem7 7509  infxpidmlem11 7513  istps2 7557  tgss2t 7587  2basgent 7591  clsval2 7635  mettriOLD 7768  metcnp 7839  lmbr 7880  causs 7906  metelcls 7916  xplmi 7923  xpcn 7926  cmsss 7947  bcthlem18 7966  bcthlem21 7969  bcthlem24 7972  bcthlem25 7973  grplcan 8025  nvmfval 8216  nvmf 8218  nvsubadd 8227  nvlmle 8281  sqcn 8283  sspmval 8339  sspival 8344  lnomul 8367  nvcnpi4 8368  nmosetre 8372  0lno 8395  sspph 8459  ubthlem12 8484  ubthlem13 8485  ubthlem14 8486  minveclem30 8518  htthlem6 8568  htthlem9 8571  hiassdit 8896  chocuni 9111  shscl 9219  fh1t 9501  fh2t 9502  cm2jt 9503  spansncv 9537  5oalem2 9540  adjsymt 9699  nmopsetretALT 9730  nmfnsetret 9744  cnvadj 9756  cnvunopt 9781  unoplint 9783  hmoplint 9805  lnopm 9863  hmopst 9883  hmopmt 9884  hmopcot 9886  adjlnopt 9957  adjmult 9963  adjaddt 9964  mdsl0 10174  ssmd2 10176  mdexch 10199  superpos 10218  chrelat2 10229  atcvatlem 10249  atcvat 10250  irredlem1 10254  irred 10258  atcvat3 10260  atcvat4 10261  mdsymlem3 10269  mdsymlem5 10271  cdj3lem2b 10298  ghomf1olem 10330

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