Theorem ad2antrr 413

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

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  simpll 421  ax11eq 1405  ax11el 1406  ax11indalem 1410  ax11inda2ALT 1411  reupick 2330  reuuniss2 2948  tz7.7 3030  fvelimab 3822  dffo4 3877  tz7.49 4017  oaordi 4238  oaass 4253  oarec 4254  omwordri 4261  omword2 4263  omass 4269  oneo 4270  oaabs 4310  nneob 4313  sbthlem8 4517  onomeneq 4583  unblem1 4603  unblem3 4605  fodomfi 4626  suppr 4650  inf3lem5 4679  infensuc 4700  r1ord 4717  ltexpq 5145  genpnnp 5173  addcanpr 5217  prlem936b 5219  supexpr 5228  cnegexlem1 5410  cnegex 5413  xrre 5634  conjmul 5855  lemulge11 5906  ledivp1 5965  xrmin1 5971  lbinfm 6130  xrsupsslem 6158  xrinfmsslem 6159  supxrre 6165  supxrun 6167  supxrunb1 6171  supxrunb2 6172  zltp1le 6263  zbtwnre 6306  btwnzge0 6357  monoord 6381  elioc2 6415  elico2 6416  elicc2 6417  elfzp1 6536  fzneuz 6544  fsequb 6549  ser1add2i 6597  ser1addi 6598  seqzfveq 6643  expnlbnd2 6745  sqr11i 6793  seq1bndi 7000  cvg2i 7012  cvganz 7014  facndiv 7033  faclbnd 7035  fsumspl 7110  fsumcmpndx2 7132  clm4lei 7171  climshfti 7194  climmullem3 7212  climsqueeze 7230  climsqueeze2 7231  climsupi 7245  climcaui 7246  caucvgi 7253  ser1cmp2i 7267  isum1p 7296  isummulc1 7302  expcnv 7323  cvgratlem2 7341  cvgratlem5 7344  fsum0diaglem2 7347  fsum0diag4 7351  ef0lem 7400  tgss2 7726  basgen2 7728  2basgen 7730  cctop 7737  elcls 7789  neips 7812  neissex 7823  cnco 7853  cnpco 7854  iscncl 7855  cnconst 7865  metxp 7919  blval 7922  bl2in 7928  blelrn 7933  blss 7938  ssblex 7941  blopn 7961  neibl 7962  lpbl 7965  metcnplem 7971  metcnp 7972  metcnp2 7973  metcnpi3 7977  metcnpi4 7978  metcnss 7983  metcnss2 7984  tgioolem 7999  lmnn 8020  lmuni 8036  lmle 8045  metelcls 8050  metcnp4 8055  metcn4 8056  cmsss 8082  bcthlem2 8085  bcthlem16 8099  bcthlem24 8107  bcthlem26 8109  grpidinvlem3 8135  grprcan 8147  sm1cnilem 8431  sspval 8466  sspn 8479  nmoub3i 8520  0lno 8534  nmlno0lem 8537  blocnilem 8548  blocni 8549  ipasslem3 8576  ipblnfi 8600  ubthlem10 8622  ubthlem11 8623  ubthlem12 8624  minveclem24 8652  htthlem6 8709  htthlem7 8710  abssinper 8795  hvaddsub4 9028  sh 9161  occon 9243  chocunii 9255  occllem6 9261  elspansn4 9579  normcan 9582  osumlem6 9666  5oalem1 9682  3oalem2 9691  nmopub2tALT 9916  unoplin 9927  nmfnleub2 9933  hmoplin 9949  nmlnop0iALT 10003  nmcopexlem5 10038  nmophmi 10044  lnopconi 10046  nmcfnexlem5 10067  lnfnconi 10073  nlelchi 10077  cnlnadjlem6 10088  rnbra 10123  kbass4 10135  kbass5 10136  stel 10225  hstel2 10230  mdsl0 10321  mdslmd1lem1 10336  mdslmd1lem2 10337  mdslmd3i 10343  mdexchi 10346  atsseq 10358  atordi 10395  irredlem1 10401  irredlem3 10403  mdsymlem2 10415  mdsymlem3 10416  mdsymlem5 10418  sumdmdii 10426  cdjreui 10443  cdj1i 10444  cdj3lem2b 10448  cdrci 10588  truni1 10593  cnrsfin 10603  cnrscoa 10604  hmphsyma 10622  qusp 10649  cnfilca 10670  iintlem1 10714  trnij 10719  homgrf 10812  imonclem 10823  ismonc 10824  cmpmon 10825  idmon 10827  isepic 10834

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 154  df-an 232

Copyright terms: Public domain