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 1361  ax11el 1362  ax11indalem 1366  ax11inda2ALT 1367  reupick 2275  reuuniss2 2886  tz7.7 2968  fvelimab 3756  dffo4 3811  tz7.49 3950  oaordi 4170  oaass 4185  oarec 4186  omwordri 4193  omword2 4195  omass 4201  oneo 4202  oaabs 4242  nneob 4245  sbthlem8 4440  onomeneq 4504  unblem1 4523  unblem3 4525  fodomfi 4546  suppr 4570  inf3lem5 4597  infensuc 4618  r1ord 4635  ltexpq 5060  genpnnp 5088  addcanpr 5132  prlem936b 5134  supexpr 5143  cnegextlem1 5325  cnegext 5328  xrret 5550  conjmult 5761  lemulge11t 5812  ledivp1t 5861  xrmin1 5867  lbinfm 6003  xrsupsslem 6031  xrinfmsslem 6032  supxrre 6038  supxrun 6040  supxrunb1 6044  supxrunb2 6045  zltp1let 6136  zbtwnre 6177  btwnzge0t 6196  monoord 6239  ser1add2 6283  ser1add 6284  elioc2t 6330  elico2t 6331  elicc2t 6332  elfzp1 6450  fzneuzt 6458  fsequb 6463  seqzfveq 6494  bernneq 6591  sqr11 6641  seq1bnd 6855  cvg2 6867  cvganz 6869  facndivt 6888  faclbnd 6890  fsumsplit 6966  fsumcmpndx2 6988  clm4le 7027  climshft 7049  climmullem3 7066  climsqueeze 7084  climsqueeze2 7085  climsup 7099  climcau 7100  caucvg 7107  ser1cmp2 7121  isum1p 7149  isummulc1 7155  expcnv 7176  cvgratlem2 7194  cvgratlem5 7197  fsum0diaglem2 7200  fsum0diag4 7204  ef0lem 7260  tgss2t 7587  basgen2t 7589  2basgent 7591  fctop 7600  cctop 7602  elcls 7654  neips 7677  neissex 7688  cnco 7718  cnpco 7719  iscncl 7720  cnconst 7730  metxp 7786  blval 7789  bl2in 7795  blelrn 7800  blss 7805  ssblex 7808  blopn 7828  neibl 7829  lpbl 7832  metcnplem 7838  metcnp 7839  metcnp2 7840  metcnpi3 7844  metcnpi4 7845  metcnss 7850  metcnss2 7851  tgioolem 7866  lmnn 7887  lmuni 7902  lmle 7911  metelcls 7916  metcnp4 7920  metcn4 7921  cmsss 7947  bcthlem2 7950  bcthlem16 7964  bcthlem24 7972  bcthlem26 7974  grpidinvlem3 8000  grprcan 8013  sm1cnilem 8294  sspval 8329  sspn 8342  nmoub3i 8381  0lno 8395  nmlno0lem 8398  blocnilem 8408  blocni 8409  ipasslem3 8436  ipblnfi 8460  ubthlem10 8482  ubthlem11 8483  ubthlem12 8484  minveclem24 8512  htthlem6 8568  htthlem7 8569  hvaddsub4t 8884  sh 9017  occont 9099  chocuni 9111  occllem6 9117  elspansn4t 9436  normcant 9439  osumlem6 9523  5oalem1 9539  3oalem2 9548  nmopub2tALT 9773  unoplint 9783  nmfnleub2t 9789  hmoplint 9805  nmlnop0ALT 9858  nmcopexlem5 9893  nmophm 9899  lnopcon 9901  nmcfnexlem5 9922  lnfncon 9928  nlelch 9932  cnlnadjlem6 9943  rnbra 9978  kbass4t 9990  kbass5t 9991  stelt 10079  hstel2t 10084  mdsl0 10174  mdslmd1lem1 10189  mdslmd1lem2 10190  mdslmd3 10196  mdexch 10199  atsseq 10211  atord 10248  irredlem1 10254  irredlem3 10256  mdsymlem2 10268  mdsymlem3 10269  mdsymlem5 10271  sumdmdi 10278  cdjreu 10293  cdj1 10294  cdj3lem2b 10298  cdrci 10417  truni1 10422  cnrsfin 10432  cnrscoa 10433  hmphsyma 10451  qusp 10466  cnfilca 10487  iintlem1 10512  trnij 10517  homgrf 10610  imonclem 10619  ismonc 10620  cmpmon 10621  idmon 10624

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