Theorem ad2antrr 440

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

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  simpll 448  simplll 452  simpllr 453  ax11eq 1754  ax11el 1755  ax11indalem 1759  ax11inda2ALT 1760  reupick 2874  tz7.7 3684  reuuniss2 3817  fvelimabOLD 4726  dffo4 4793  reiotass2 5111  onfununi 5116  oaordi 5227  oaass 5243  oarec 5244  omwordri 5251  omword2 5253  omass 5259  oneo 5260  oaabs 5309  nneob 5312  ac6sfilem3 5508  sbthlem8 5517  onomeneq 5612  unblem1 5633  unblem3 5635  fodomfi 5656  suppr 5680  ordiso 5683  ordtypelem6 5689  ordtypelem7 5690  hartoglem 5692  hartog 5693  inf3lem5 5723  infensuc 5745  r1ord 5766  omsubsdomlem2 5880  genpnnp 6260  addcanpr 6304  prlem936b 6306  supexpr 6315  cnegexlem1 6499  cnegex 6502  xrre 6744  conjmul 6975  lemulge11 7030  ledivp1 7088  xrmin1 7094  lbinfm 7257  xrsupsslem 7285  xrinfmsslem 7286  supxrre 7292  supxrun 7294  supxrunb1 7298  supxrunb2 7299  zltp1le 7390  zbtwnre 7434  btwnzge0 7486  modid 7512  monoord 7523  elioc2 7558  elico2 7559  elicc2 7560  elfzp1 7683  fzneuz 7697  fsequb 7702  ser1add2i 7751  ser1addi 7752  seqzfveq 7797  expnlbnd2 7903  digit1 7905  sqr11i 7953  seq1bndi 8162  cvg2i 8174  cvganz 8176  facndiv 8195  faclbnd 8197  fsumsplit 8280  fsumcmpndx2 8302  clm4lei 8341  climshfti 8364  climmullem3 8382  climsqueeze 8400  climsqueeze2 8401  climsupi 8415  climcaui 8416  caucvgi 8423  ser1cmp2i 8437  isum1p 8467  isummulc1 8473  expcnv 8494  cvgratlem5 8516  fsum0diaglem2 8519  fsum0diag4 8523  ef0lem 8572  basgen2 8909  2basgen 8911  fctop 8920  cctop 8922  neips 9003  cnpnei 9043  cnpco 9046  iscncl 9047  cnconst 9057  metxp 9111  blval 9114  bl2in 9120  blelrn 9125  blss 9130  ssblex 9133  blopn 9153  neibl 9154  lpbl 9157  metequiv 9158  metcnplem 9164  metcnp 9165  metcnpi3 9170  metcnpi4 9171  metcnss 9176  metcnss2 9177  tgioolem 9192  lmnn 9213  lmuni 9229  lmle 9238  metelcls 9243  metcnp4 9248  metcn4 9249  cmsss 9275  bcthlem2 9278  bcthlem16 9292  bcthlem24 9300  bcthlem26 9302  grpidinvlem3 9330  grprcan 9347  ssga 9455  vacnlem3 9669  sm1cnilem 9686  sspval 9721  sspn 9734  nmoub3i 9775  0lno 9790  nmlno0lem 9793  blocnilem 9804  blocni 9805  ipasslem3 9833  ipblnfi 9857  ubthlem10 9881  ubthlem11 9882  ubthlem12 9883  ubthlem12OLD 9884  minveclem24 9913  htthlem6 9972  htthlem7 9973  spwpr4 10006  abssinper 10062  indexfi 10174  fipreima 10175  cdrci 10182  tx2cn 10224  txcn 10227  2txcn 10229  subcld 10254  subtopmetlem 10255  subtopmet 10256  filrn 10293  elfilmap3 10314  flimopn 10321  dirtr 10356  exidu1 10373  hvaddsub4 10578  sh 10711  occon 10793  chocunii 10805  elspansn4 11129  normcan 11132  osumlem6 11218  5oalem1 11234  3oalem2 11243  nmopub2tALT 11470  unoplin 11481  nmfnleub2 11487  hmoplin 11503  nmlnop0iALT 11557  nmcopexlem5 11592  nmophmi 11598  lnopconi 11600  nmcfnexlem5 11621  lnfnconi 11627  nlelchi 11631  cnlnadjlem6 11642  rnbra 11678  kbass4 11690  stel 11786  hstel2 11791  mdsl0 11882  mdslmd1lem2 11898  mdslmd3i 11904  mdexchi 11907  atsseq 11919  atordi 11956  irredlem1 11962  irredlem3 11964  mdsymlem3 11977  mdsymlem5 11979  sumdmdii 11987  cdjreui 12004  cdj1i 12005  cdj3lem2b 12009  dfon2lem6 13854  dfon2lem8 13856  preddowncl 13907  poseq 13954  soseq 13955  wfrlem4 13960  sltasym 14010  axdenselem3 14021  axdenselem5 14023  axdenselem6 14024  axdense 14027  axfelem5 14035  npincppr 14501  cur1vald 14547  domrancur1c 14550  tostos 14637  toplat 14638  curgrpact 14735  muldisc 14824  svli2 14826  svs3 14830  truni1 14849  cnrsfin 14868  cnrscoa 14869  hmphsyma 14882  qusp 14908  cnfilca 14927  conttnf 14944  iscnp3 14946  iintlem1 15010  trnij 15015  lvsovso2 15039  supnuf 15041  dualcat2 15133  homgrf 15151  imonclem 15162  ismonc 15163  cmpmon 15164  idmon 15166  isepic 15173  idsubfun 15206  cptarc 15242  eltintpar 15276  cartarlim 15282  elicc3 15362  ioodisj 15364  finminlem 15367  elfiun 15369  fictblem 15370  finsschain 15373  ordisoOLD 15374  ordtypelem6OLD 15380  ordtypelem7OLD 15381  hartoglemOLD 15383  hartogOLD 15384  omsubsdomlem2OLD 15389  cncls 15419  subsubtop 15423  cnsubsp2 15427  compsublem 15430  compsub 15431  cptclsscpt 15432  hscptsscld 15434  alexsublem3 15439  alexsublem4 15440  alexsub 15441  cnconn 15444  reconnlem1 15446  reconnlem2 15447  reconnlem3 15448  reconnlem4 15449  reconnlem5 15450  reconn 15451  2ndcsb 15476  2ndcctbss 15478  isfne3 15482  topfneec 15501  locfincf 15516  comppfsc 15517  neibastop1 15518  neibastop2lem3 15521  neibastop2lem4 15522  neibastop2 15523  neibastop3 15524  topjoin 15527  fnemeet2 15529  fbasfip 15556  supfil 15560  isufil2 15565  filssufillem 15570  ufileulem 15572  ufileu 15573  uffixfr 15575  fixufil 15576  ufinffr 15578  ufilen 15579  filcon 15580  limfilcf 15587  cnpfillim 15589  rnelfmlem 15592  rnelfm 15593  fmfnfmlem1 15594  fmfnfmlem2 15595  fmfnfmlem3 15596  fmfnfmlem4 15597  fmfnfm 15598  flimfcnp 15602  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscnp 15618  fcluscomplem 15620  isfclusf 15625  filnetlem4 15643  filnetlem5 15644  filnet 15645  enf1f1o 15720  upixp 15729  indexfiOLD 15755  fipreimaOLD 15756  frfi 15771  filbcmb 15776  sdc 15811  fdc 15812  incsequz 15815  nnubfi 15818  nninfnub 15819  fsumlt1 15831  subspabs 15840  blssp 15844  mettrifi 15847  geomcau 15849  metdcn 15853  icoopnst 15876  cnimass 15888  cnres 15889  lmtlm 15908  txsubsp 15912  txcld 15914  txmet 15925  sstotbnd 15936  totbndss 15937  isbnd3 15941  bndss 15942  totbndbnd 15944  ismtyhmeolem 15950  ismtybndlem 15952  heiborlem12 15966  heiborlem13 15967  heiborlem16 15970  heiborlem23 15977  heiborlem32 15986  heiborlem34 15988  heiborlem35 15989  heiborlem36 15990  heiborlem42 15996  bfplem9 16006  rrncms 16019  rrntotbndlem1 16020  rrntotbndlem2 16021  rrntotbnd 16022  iccbnd 16026  ghomco 16040  phtpyco 16056  reparpht 16065  pcohtpy 16083  pcoass 16085  pi1gp 16095  idlnegcl 16170  unichnidl 16179  keridl 16180  isfldidl 16216  strdif 16719  glbcon 17028  hlatmstc 17047  atcvrj2b 17069  cvrat4 17076  cvrat42 17077  ps-1 17078  grpidinvlem3NEW 17111  grprcanNEW 17122  linepsub 17232  pmapat 17243  pmapglbx 17251  paddasslem5 17285  pmapjoin 17313  pmapjat 17314  polval2 17319  pexmid 17377

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 164  df-an 242

Copyright terms: Public domain