Theorem ad2antrl 406

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 389	. 2 |- ((ph /\ th) -> ps)
3	2	adantl 388	1 |- ((ch /\ (ph /\ th)) -> ps)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simprl 414  tz7.7 2963  onint 2996  elxp5 3440  tz7.48lem 3940  oalimcl 4178  sdomdomtr 4449  mapenlem2 4470  mapunen 4482  isfinite2 4523  fodomfi 4540  aceq3 4705  aceq5 4712  axacnd 4936  ltapq 5048  ltexprlem7 5120  cnegextlem2 5318  divdivmult 5751  conjmult 5753  lt2mul2divt 5822  lediv12it 5844  ledivp1t 5853  zltp1let 6128  peano2uz2 6149  uzwo5OLD 6159  uzwo3lem1 6164  eluzp1m1t 6365  climrecl 7047  climmullem1 7056  climmullem3 7058  climmullem4 7059  climmullem5 7060  climsup 7091  caucvglem6 7098  serzf0 7105  ser1f0 7106  cvgratlem3 7187  cvgratlem5 7189  acdc3lem 7428  acdc2lem2 7431  acdc5lem2 7434  acdclem 7436  infxpidmlem1 7495  tgclt 7566  clsval2 7627  qdensere 7691  cnconst 7719  opnuni 7808  metcnp 7826  metcnpi3 7831  metcnpi4 7832  metcni2 7834  causs 7890  xpcn 7910  cmsss 7931  bcthlem17 7949  grpidinvlem1 7982  grpidinvlem3 7984  grprcan 7997  vcsubdir 8112  sqcn 8270  nmlnoubi 8388  blocnilem 8395  ubthlem3 8462  ubthlem8 8467  ocsh 9072  projlem26 9127  pjpj0 9170  shmods 9277  osumlem7 9501  5oalem2 9517  3oalem2 9525  eigpos 9679  nmopub2tALT 9750  nmfnleub2t 9766  nmcopexlem5 9870  lnopcon 9878  nmcfnexlem5 9899  lnfncon 9905  nmopco 9942  kbass3t 9963  mdslmd1lem1 10160  mdslmd1lem2 10161  atom1d 10188  irredlem2 10226  irredlem4 10228  mdsymlem3 10240  mdsymlem5 10242  sumdmdi 10249  sumdmdlem 10252  sumdmdlem2 10253  qusp 10430  iintlem1 10476  trnij 10481  domcmpd 10523  cmpida 10551  cmpmon 10585

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