Theorem ad2antrl 415

Description: Deduction adding conjuncts to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem ad2antrl

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

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  simprl 423  tz7.7 3030  onint 3063  elxp5 3511  tz7.48lem 4013  oalimcl 4252  sdomdomtr 4532  mapenlem2 4555  mapunen 4567  fodomfi 4626  aceq3 4795  aceq5 4802  axacnd 5029  ltapq 5141  ltexprlem7 5213  cnegexlem2 5411  divdivmul 5853  conjmul 5855  ltdivmul 5925  ledivmul 5927  lt2mul2div 5931  lediv12a 5956  ledivp1 5965  zltp1le 6263  peano2uz2 6286  uzwo5OLD 6296  uzwo3lem1 6301  modadd1 6380  iooshf 6421  ioojoin 6442  eluzp1m1 6459  climrecl 7200  climmullem1 7210  climmullem3 7212  climmullem4 7213  climmullem5 7214  climsupi 7245  caucvglem6 7252  serzf0i 7259  ser1f0i 7260  cvgratlem3 7342  cvgratlem5 7344  acdc3lem 7578  acdc2lem2 7581  acdc5lem2 7584  acdclem 7586  infxpidmlem1 7644  tgcl 7713  clsval2 7770  qdensere 7836  cnconst 7865  opnuni 7953  metcnp 7972  metcnpi3 7977  metcnpi4 7978  metcni2 7980  causs 8040  xpcn 8061  cmsss 8082  bcthlem17 8100  grpidinvlem1 8133  grpidinvlem3 8135  grprcan 8147  vcsubdir 8259  sqcn 8419  nmlnoubi 8540  blocnilem 8548  ubthlem3 8615  ubthlem8 8620  ocsh 9239  projlem26 9294  pjpj0i 9338  shmodsi 9445  osumlem7 9667  5oalem2 9683  3oalem2 9691  eigposi 9845  nmopub2tALT 9916  nmfnleub2 9933  nmcopexlem5 10038  lnopconi 10046  nmcfnexlem5 10067  lnfnconi 10073  nmopcoi 10111  kbass3 10134  mdslmd1lem1 10336  mdslmd1lem2 10337  atom1d 10364  irredlem2 10402  irredlem4 10404  mdsymlem3 10416  mdsymlem5 10418  sumdmdii 10426  sumdmdlem 10429  sumdmdlem2 10430  qusp 10649  usinuniop 10703  iintlem1 10714  trnij 10719  domcmpd 10761  cmpida 10789  cmpmon 10825

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