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 2969  onint 3002  elxp5 3450  tz7.48lem 3950  oalimcl 4187  sdomdomtr 4458  mapenlem2 4479  mapunen 4491  isfinite2 4532  fodomfi 4549  aceq3 4716  aceq5 4723  axacnd 4947  ltapq 5059  ltexprlem7 5131  cnegextlem2 5329  divdivmult 5761  conjmult 5763  lt2mul2divt 5832  lediv12it 5854  ledivp1t 5863  zltp1let 6138  peano2uz2 6159  uzwo5OLD 6169  uzwo3lem1 6174  eluzp1m1t 6378  climrecl 7063  climmullem1 7073  climmullem3 7075  climmullem4 7076  climmullem5 7077  climsup 7108  caucvglem6 7115  serzf0 7122  ser1f0 7123  cvgratlem3 7204  cvgratlem5 7206  acdc3lem 7445  acdc2lem2 7448  acdc5lem2 7451  acdclem 7453  infxpidmlem1 7512  tgclt 7584  clsval2 7645  qdensere 7711  cnconst 7740  opnuni 7830  metcnp 7849  metcnpi3 7854  metcnpi4 7855  metcni2 7857  causs 7917  xpcn 7938  cmsss 7959  bcthlem17 7977  grpidinvlem1 8010  grpidinvlem3 8012  grprcan 8025  vcsubdir 8139  sqcn 8298  nmlnoubi 8416  blocnilem 8423  ubthlem3 8490  ubthlem8 8495  ocsh 9111  projlem26 9166  pjpj0 9210  shmods 9317  osumlem7 9541  5oalem2 9557  3oalem2 9565  eigpos 9719  nmopub2tALT 9790  nmfnleub2t 9807  nmcopexlem5 9911  lnopcon 9919  nmcfnexlem5 9940  lnfncon 9946  nmopco 9984  kbass3t 10007  mdslmd1lem1 10208  mdslmd1lem2 10209  atom1d 10236  irredlem2 10274  irredlem4 10276  mdsymlem3 10288  mdsymlem5 10290  sumdmdi 10298  sumdmdlem 10301  sumdmdlem2 10302  qusp 10489  iintlem1 10548  trnij 10553  domcmpd 10595  cmpida 10623  cmpmon 10657

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