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 4454  onomeneq 4519  unblem1 4540  unblem3 4542  fodomfiOLD 4566  suppr 4590  inf3lem5 4617  infensuc 4638  r1ord 4655  ltexpq 5080  genpnnp 5108  addcanpr 5152  prlem936b 5154  supexpr 5163  cnegextlem1 5345  cnegext 5348  xrret 5569  conjmult 5797  lemulge11t 5848  ledivp1t 5905  xrmin1 5911  lbinfm 6048  xrsupsslem 6076  xrinfmsslem 6077  supxrre 6083  supxrun 6085  supxrunb1 6089  supxrunb2 6090  zltp1let 6181  zbtwnre 6221  btwnzge0t 6245  monoord 6294  ser1add2 6338  ser1add 6339  elioc2t 6390  elico2t 6391  elicc2t 6392  elfzp1 6510  fzneuzt 6518  fsequb 6523  seqzfveq 6554  sqr11 6703  seq1bnd 6910  cvg2 6922  cvganz 6924  facndivt 6943  faclbnd 6945  fsumsplit 7020  fsumcmpndx2 7042  clm4le 7081  climshft 7104  climmullem3 7122  climsqueeze 7140  climsqueeze2 7141  climsup 7155  climcau 7156  caucvg 7163  ser1cmp2 7177  isum1p 7206  isummulc1 7212  expcnv 7233  cvgratlem2 7251  cvgratlem5 7254  fsum0diaglem2 7257  fsum0diag4 7261  ef0lem 7310  tgss2t 7637  basgen2t 7639  2basgent 7641  fctopOLD 7650  cctop 7652  elcls 7704  neips 7727  neissex 7738  cnco 7768  cnpco 7769  iscncl 7770  cnconst 7780  metxp 7834  blval 7837  bl2in 7843  blelrn 7848  blss 7853  ssblex 7856  blopn 7876  neibl 7877  lpbl 7880  metcnplem 7886  metcnp 7887  metcnp2 7888  metcnpi3 7892  metcnpi4 7893  metcnss 7898  metcnss2 7899  tgioolem 7914  lmnn 7935  lmuni 7951  lmle 7960  metelcls 7965  metcnp4 7970  metcn4 7971  cmsss 7997  bcthlem2 8000  bcthlem16 8014  bcthlem24 8022  bcthlem26 8024  grpidinvlem3 8050  grprcan 8063  sm1cnilem 8347  sspval 8382  sspn 8395  nmoub3i 8436  0lno 8450  nmlno0lem 8453  blocnilem 8464  blocni 8465  ipasslem3 8492  ipblnfi 8516  ubthlem10 8538  ubthlem11 8539  ubthlem12 8540  minveclem24 8568  htthlem6 8625  htthlem7 8626  spwpr3OLD 8662  abssinper 8712  hvaddsub4t 8945  sh 9078  occont 9160  chocuni 9172  occllem6 9178  elspansn4t 9496  normcant 9499  osumlem6 9583  5oalem1 9599  3oalem2 9608  nmopub2tALT 9833  unoplint 9844  nmfnleub2t 9850  hmoplint 9866  nmlnop0ALT 9920  nmcopexlem5 9955  nmophm 9961  lnopcon 9963  nmcfnexlem5 9984  lnfncon 9990  nlelch 9994  cnlnadjlem6 10005  rnbra 10040  kbass4t 10052  kbass5t 10053  stelt 10141  hstel2t 10146  mdsl0 10237  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd3 10259  mdexch 10262  atsseq 10274  atord 10311  irredlem1 10317  irredlem3 10319  mdsymlem2 10331  mdsymlem3 10332  mdsymlem5 10334  sumdmdi 10342  cdjreu 10359  cdj1 10360  cdj3lem2b 10364  cdrci 10494  truni1 10499  cnrsfin 10509  cnrscoa 10510  hmphsyma 10528  qusp 10555  cnfilca 10583  cnfilcaOLD 10584  iintlem1 10632  trnij 10637  homgrf 10730  imonclem 10741  ismonc 10742  cmpmon 10743  idmon 10745

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