Theorem ad2antrr 404

Description: Deduction adding conjuncts to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem ad2antrr

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

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  simpll 412  ax11eq 1363  ax11el 1364  ax11indalem 1368  ax11inda2ALT 1369  reupick 2279  reuuniss2 2891  tz7.7 2973  fvelimab 3765  dffo4 3820  tz7.49 3959  oaordi 4180  oaass 4195  oarec 4196  omwordri 4203  omword2 4205  omass 4211  oneo 4212  oaabs 4252  nneob 4255  sbthlem8 4452  onomeneq 4516  unblem1 4535  unblem3 4537  fodomfi 4558  suppr 4582  inf3lem5 4609  infensuc 4630  r1ord 4647  ltexpq 5072  genpnnp 5100  addcanpr 5144  prlem936b 5146  supexpr 5155  cnegextlem1 5337  cnegext 5340  xrret 5561  conjmult 5785  lemulge11t 5836  ledivp1t 5893  xrmin1 5899  lbinfm 6036  xrsupsslem 6064  xrinfmsslem 6065  supxrre 6071  supxrun 6073  supxrunb1 6077  supxrunb2 6078  zltp1let 6169  zbtwnre 6209  btwnzge0t 6232  monoord 6280  ser1add2 6324  ser1add 6325  elioc2t 6376  elico2t 6377  elicc2t 6378  elfzp1 6496  fzneuzt 6504  fsequb 6509  seqzfveq 6540  sqr11 6689  seq1bnd 6895  cvg2 6907  cvganz 6909  facndivt 6928  faclbnd 6930  fsumsplit 7005  fsumcmpndx2 7027  clm4le 7066  climshft 7089  climmullem3 7107  climsqueeze 7125  climsqueeze2 7126  climsup 7140  climcau 7141  caucvg 7148  ser1cmp2 7162  isum1p 7191  isummulc1 7197  expcnv 7218  cvgratlem2 7236  cvgratlem5 7239  fsum0diaglem2 7242  fsum0diag4 7246  ef0lem 7295  tgss2t 7622  basgen2t 7624  2basgent 7626  fctop 7635  cctop 7637  elcls 7689  neips 7712  neissex 7723  cnco 7753  cnpco 7754  iscncl 7755  cnconst 7765  metxp 7819  blval 7822  bl2in 7828  blelrn 7833  blss 7838  ssblex 7841  blopn 7861  neibl 7862  lpbl 7865  metcnplem 7871  metcnp 7872  metcnp2 7873  metcnpi3 7877  metcnpi4 7878  metcnss 7883  metcnss2 7884  tgioolem 7899  lmnn 7920  lmuni 7936  lmle 7945  metelcls 7950  metcnp4 7955  metcn4 7956  cmsss 7982  bcthlem2 7985  bcthlem16 7999  bcthlem24 8007  bcthlem26 8009  grpidinvlem3 8035  grprcan 8048  sm1cnilem 8332  sspval 8367  sspn 8380  nmoub3i 8421  0lno 8435  nmlno0lem 8438  blocnilem 8449  blocni 8450  ipasslem3 8477  ipblnfi 8501  ubthlem10 8523  ubthlem11 8524  ubthlem12 8525  minveclem24 8553  htthlem6 8610  htthlem7 8611  spwpr3OLD 8647  abssinper 8697  hvaddsub4t 8930  sh 9063  occont 9145  chocuni 9157  occllem6 9163  elspansn4t 9481  normcant 9484  osumlem6 9568  5oalem1 9584  3oalem2 9593  nmopub2tALT 9818  unoplint 9829  nmfnleub2t 9835  hmoplint 9851  nmlnop0ALT 9905  nmcopexlem5 9940  nmophm 9946  lnopcon 9948  nmcfnexlem5 9969  lnfncon 9975  nlelch 9979  cnlnadjlem6 9990  rnbra 10025  kbass4t 10037  kbass5t 10038  stelt 10126  hstel2t 10131  mdsl0 10222  mdslmd1lem1 10237  mdslmd1lem2 10238  mdslmd3 10244  mdexch 10247  atsseq 10259  atord 10296  irredlem1 10302  irredlem3 10304  mdsymlem2 10316  mdsymlem3 10317  mdsymlem5 10319  sumdmdi 10327  cdjreu 10344  cdj1 10345  cdj3lem2b 10349  cdrci 10466  truni1 10471  cnrsfin 10481  cnrscoa 10482  hmphsyma 10500  qusp 10515  cnfilca 10537  iintlem1 10575  trnij 10580  homgrf 10673  imonclem 10682  ismonc 10683  cmpmon 10684  idmon 10687

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