Theorem adantrr 431

Description: Deduction adding a conjunct to antecedent.

Hypothesis

Ref	Expression
adant2.1	|- ((ph /\ ps) -> ch)

Assertion

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

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 402	. . 3 |- (ph -> (ps -> ch))
3	2	adantrd 427	. 2 |- (ph -> ((ps /\ th) -> ch))
4	3	imp 377	1 |- ((ph /\ (ps /\ th)) -> ch)

Syntax hints:   -> wi 3   /\ wa 240

This theorem is referenced by:  ad2ant2r 445  ad2ant2lr 446  anabss1 557  3ad2antr1 1041  sbcom 1632  ax11eq 1754  ax11el 1755  ifboth 3002  po2nr 3599  sotric 3615  sotrieq 3616  tz7.7 3684  ordsucun 3905  opelxp1 4026  isocnv 4873  isomin 4876  isoini 4877  1stconst 5070  oalim 5212  omlim 5213  oaass 5243  omordi 5245  omwordri 5251  odi 5258  oen0 5261  oewordri 5267  oeworde 5268  dom2d 5463  ssenen 5598  ssfi 5630  hartog 5693  inf3lem6 5724  rankxplim3 5825  aceq5lem4 5900  aceq6b 5904  unidom 5970  axacndlem4 6114  ltapq 6228  ltmpq 6229  ltexpq 6232  ltexprlem6 6299  ssgt0sr 6369  add4OLD 6492  2addsub 6548  mul4 6581  muladd 6582  muladdOLD 6583  xrlttr 6728  ltleadd 6829  divmul3 6898  rec11r 6955  divadddiv 6960  divdivdivOLD 6962  lemul2a 7021  lemul12b 7024  ltmuldiv2 7047  ltdivmul 7049  ledivmul 7051  ltdivmul2 7053  lt2mul2div 7054  ledivmul2 7056  lemuldiv2 7059  ltdiv23 7075  lediv23 7076  suprleub 7268  infmrcl 7278  xrsupsslem 7285  xrinfmsslem 7286  supxrunb1 7298  supxrunb2 7299  supxrleub 7308  zextlt 7402  zmax 7433  qbtwnre 7459  modid 7512  modadd1 7518  modmul1 7519  iooshf 7564  icounlem 7581  ioojoin 7585  exprec 7837  exprecOLD 7838  expsubOLD 7842  expordi 7845  expord2 7849  sqlecan 7887  lenegsq 8137  seq1ublem 8163  fsumcom 8288  fsumshft 8291  2climnn 8362  2climnn0 8363  climge0 8372  climaddlem3 8376  climmullem1 8380  climmullem3 8382  climmullem5 8384  climmullem8 8387  climsqueeze 8400  climsqueeze2 8401  climcaui 8416  serzf0i 8429  ser1cmp2i 8437  cvgratlem2ALT 8510  cvgratlem2 8513  cvgratlem5 8516  fsum0diaglem2 8519  mulc1cncf 8541  acdc3lem 8754  acdclem 8763  infxpidmlem7 8827  infxpidmlem12 8832  eltg2 8889  tgcl 8894  tgval3 8895  tgss2 8907  2basgen 8911  txbas 8933  iscld 8945  ntrss 8964  ssnei2 9006  neindisj 9007  islp2 9023  cnpcl 9040  dnsconst 9065  ismsg 9077  blss 9130  blssex 9131  metcnp 9165  metcnpi3 9170  metcnpi4 9171  metcni2 9173  tgioolem 9192  lmss 9231  lmle 9238  metelcls 9243  metcnp4 9248  xplmi 9251  xpcn 9254  lmcau 9274  cmsss 9275  bcthlem11 9287  bcthlem15 9291  bcthlem18 9294  bcthlem19 9295  bcthlem20 9296  bcthlem21 9297  bcthlem24 9300  grpidinv 9332  grprcan 9347  grpinvid1 9356  grpinvid2 9357  grplcan 9359  abl4 9413  gapmlem 9461  isring 9465  nvsubadd 9607  nvabs 9633  vacnlem3 9669  vacnlem6 9672  va1cnlem 9684  nvcnpi3 9761  nvcnpi4 9762  sspph 9856  ubthlem3 9874  ubthlem9 9880  ubthlem11 9882  ubthlem12 9883  ubthlem12OLD 9884  ubthlem14 9887  spwpr4 10006  xp1st 10155  oprabopabf 10157  uptx 10226  subtopmetlem 10255  subtopmet 10256  fgbas 10286  hausfillim 10303  elfilmap2 10313  cncomp 10331  hvadd4 10537  hvaddsub4 10578  chocunii 10805  occllem6 10811  shscli 10914  pjspansn 11133  fh1 11194  fh2 11195  cm2j 11196  spansncvi 11232  5oalem2 11235  5oalem5 11238  5oalem6 11239  3oalem2 11243  hoadd4 11347  cnvunop 11479  bralnfn 11509  eighmorth 11525  hmops 11582  hmopm 11583  hmopco 11585  lnopconi 11600  lnfnconi 11627  adjlnop 11656  adjmul 11662  adjadd 11663  nmopcoi 11665  kbass6 11692  hstle 11802  stlesi 11813  strlem3a 11824  hstrlem3a 11832  mdsl0 11882  mdexchi 11907  atom1d 11925  superpos 11926  cvexchlem 11940  atomli 11954  atcvatlem 11957  irredlem2 11963  irredlem3 11964  atcvat4i 11969  mdsymlem1 11975  mdsymlem3 11977  mdsymlem5 11979  mdsymlem6 11980  sumdmdlem 11990  sumdmdlem2 11991  cdj1i 12005  cdj3lem2b 12009  fseq1cl 13619  dvdsmulcr 13683  ndvdsadd 13711  eucalgf 13751  eucalginv 13752  eucalglt 13753  mulgcdlem2 13757  isprm3 13776  dfon2lem6 13854  wfrlem3 13959  axfelem12 14042  axfelem13 14043  axfelem14 14044  nndivsub 14258  mulinvsca 14823  truni3 14851  dualcat2 15133  iepiclem 15172  finminlem 15367  hartogOLD 15384  subntr 15425  cnsubsp2 15427  hscptsscld 15434  compfipin0lem 15435  compfipin0 15436  alexsublem4 15440  dfcon2 15442  cnconn 15444  reconnlem1 15446  reconnlem5 15450  reconn 15451  iccconn 15453  2ndc1stc 15477  isfne 15480  fneint 15486  isref 15488  comppfsc 15517  neibastop1 15518  neibastop2lem2 15520  neibastop3 15524  topjoin 15527  fnejoin1 15530  ist1-2 15542  fbasfip 15556  filfinnfr 15561  filssufillem 15570  ufileu 15573  filcon 15580  cnpfillim 15589  fmfnfmlem2 15595  fclusnei 15607  fcluscf 15612  flimfnfcls 15615  fcluscnplem 15617  fcluscomplem 15620  fclusfnei 15626  fclsfcnp 15631  tailfb 15639  anim12da 15647  eropreu 15733  fimax 15746  frinfm 15758  infmrgelb 15766  pofun 15772  filbcmb 15776  sdclem2 15810  sdc 15811  seqpo 15814  neificl 15841  blssp 15844  blhalf 15846  mettrifi 15847  geomcau 15849  caushft 15851  lincmb01icc 15879  addccncf 15883  sub1cncf 15885  sub2cncf 15886  cnimass 15888  cnres 15889  cnresima 15891  hmeoopn 15899  hmeocld 15900  txcld 15914  txmet 15925  sstotbnd 15936  totbndss 15937  ismtycnv 15949  ismtyhmeolem 15950  ismtyhmeo 15951  ismtyres 15954  heiborlem16 15970  rrndstprj2 16018  rrncms 16019  rrntotbnd 16022  ghomco 16040  ghomdiv 16041  grpkerinj 16042  phtpycom 16050  pcohtpylem3 16082  pcohtpy 16083  pi1gp 16095  isdivrng2 16111  rnghomco 16128  rngisocnv 16135  rngisoco 16136  crngm4 16151  crnghomfo 16154  isidlc 16163  ispridl2 16186  ispridlc 16218  lubun 16899  lubunNEW 16900  omllaw3 16966  omlfh1 16978  cvratlem 17061  cvrat3 17075  cvrat4 17076  ps2 17079  grpidinvNEW 17113  grprcanNEW 17122  grpinvid1NEW 17131  grpinvid2NEW 17132  grplcanNEW 17134  elpaddn0 17261  paddasslem10 17290

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