Theorem adantll 392

Description: Deduction adding a conjunct to antecedent.

Hypothesis

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

Assertion

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

Proof of Theorem adantll

Step	Hyp	Ref	Expression
1		adant2.1	. . . 4 |- ((ph /\ ps) -> ch)
2	1	ex 371	. . 3 |- (ph -> (ps -> ch))
3	2	adantl 388	. 2 |- ((th /\ ph) -> (ps -> ch))
4	3	imp 348	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 221

This theorem is referenced by:  ad2ant2l 408  ad2ant2lr 410  3ad2antl3 817  3adant1l 858  ax11eq 1402  ax11el 1403  reu3 1977  tz7.7 3001  limsssuc 3204  ssimaex 3879  eqfnfv 3909  eqfnfv2 3911  dffo4 3934  fopab2 3937  fconst2g 3959  isotr 4011  isotrALT 4012  curry1 4193  curry2 4196  oe0 4297  oesuc 4302  oecl 4308  oaordi 4316  oawordri 4320  oaass 4331  omordi 4333  omword2 4341  omlimcl 4345  odi 4346  omass 4347  oeoe 4362  nneob 4395  omsmolem 4396  dom2d 4545  ac6sfi 4591  sbthlem9 4600  enen1 4622  sdomen1 4626  sdomen2 4627  mapenlem2 4637  mapxpen 4642  xpmapenlem3 4645  xpmapenlem4 4646  php3 4662  onomeneq 4665  finsucdom 4673  fiint 4703  fodomfi 4709  fodomfib 4710  supmo 4719  ac6lem 4900  zorn2lem6 4939  axrepnd 5100  axpowndlem2 5104  axpowndlem4 5106  axinfndlem1 5111  axinfnd 5112  axacndlem4 5116  axacndlem5 5117  axacnd 5118  ltexpq 5234  ltrpq 5239  prcdpq 5251  addclprlem2 5273  prlem934b 5292  ltexpri 5303  prlem936b 5308  ssgt0sr 5371  cnegex 5502  1re 5589  axsup 5661  xrlttr 5707  ltleadd 5799  divadddiv 5923  lt2mul2div 6016  lediv12a 6041  nn2ge 6087  infmrcl 6237  xrsupsslem 6244  xrinfmsslem 6245  supxrunb1 6257  supxrunb2 6258  zextle 6360  modadd1 6477  modmul1 6478  iooin 6498  elioc2 6516  elico2 6517  elicc2 6518  elfz2nn0 6625  fzaddel 6630  fzsuc 6636  fzrev 6642  fzrevral 6650  fsequb2 6655  mulexp 6788  expadd 6791  expmul 6792  expmwordi 6803  expnbnd 6852  sqr2irrlem3 6927  seq1ublem 7114  cau2i 7116  caubndi 7129  fsum1ps 7221  fsumrev 7232  fsumshft 7234  fsumshftm 7235  fsummulc1 7236  fsumdivc 7238  fsumdivcALT 7239  fsum2mul 7240  climshfti 7307  climaddlem3 7319  climaddc2 7322  climmullem4 7326  climmullem5 7327  climmullem8 7330  climsub 7333  climsupi 7358  climcaui 7359  caucvglem5 7364  caucvglem6 7365  caucvgi 7366  cvgcmp3ci 7390  cvgratlem1 7455  fsum0diag4 7466  acdc3lem 7697  acdc2lem1 7700  acdc5lem1 7703  acdclem 7706  unbenlem 7716  infpnlem1 7718  ruclem13 7734  infxpidmlem1 7764  infxpidmlem11 7774  infxpidmlem12 7775  tgss2 7849  elcls 7914  cnconst 7990  metxp 8044  metcnplem 8097  metcnp2 8099  metcnss 8109  metcnss2 8110  tgioolem 8125  lmconst 8145  lmnn 8146  iscaunns 8155  metcnp4lem2 8180  metcnp4 8181  xplmi 8184  xpcn 8187  bopcnlem2 8193  iscms2lem3 8202  iscms2lem5 8204  bcthlem2 8211  bcthlem26 8235  bcthlem29 8238  grpidinvlem3 8263  grpidinv 8265  grpideu 8266  isgrp2i 8293  vacnlem5 8586  va1cnlem 8599  sm1cnilem 8601  nmoub3i 8690  nmlno0lem 8708  nmlnoubi 8711  blocnilem 8719  blocni 8720  ipasslem3 8748  ipblnfi 8772  ubthlem5 8791  ubthlem12 8798  ubthlem12OLD 8799  spwpr2 8920  hvaddsub4 9221  chocunii 9448  occllem6 9454  shsel3 9555  chj4 9734  spansncol 9767  5oalem2 9878  3oalem2 9886  adjsym 10039  cnvadj 10096  nmopub2tALT 10113  unoplin 10124  counop 10125  nmfnleub2 10130  hmoplin 10146  brafnmul 10155  nmlnop0iALT 10199  nmopun 10218  nmcopexlem6 10235  lnopconi 10242  nmcfnexlem6 10264  lnfnconi 10269  nlelchi 10273  riesz3i 10274  riesz1 10277  cnlnadjlem2 10280  cnlnadjlem6 10284  adjmul 10304  adjadd 10305  bra11 10321  cnvbraval 10323  kbass5 10333  kbass6 10334  leop2 10337  leopadd 10345  leopmuli 10346  leoptri 10349  leopnmid 10351  nmopleid 10352  pj3si 10416  hstel2 10427  cvcon3 10492  dmdmd 10508  dmdbr5 10516  mdsl0 10518  mdslmd1lem1 10533  mdslmd1lem2 10534  mdslmd3i 10540  superpos 10562  irredlem2 10600  irredlem3 10601  mdsymlem3 10614  mdsymlem5 10616  mdsymlem6 10617  sumdmdlem 10627  cdjreui 10641  cdj1i 10642  cdj3i 10650  toplat 10884  cdrci 10994  fgsb 11082  fgsb2 11086  idsubfun 11312  elicc3 11410  fiuni 11420  fictblem 11422  inficlALT 11424  ordiso 11426  ordtypelem6 11432  ordtypelem7 11433  hartog 11436  cnpnei 11472  subsubtop 11479  compsub 11488  hscptsscld 11491  cncomp 11494  comptoppr 11495  alexsublem4 11499  connsub 11502  cnconn 11503  conntoppr 11504  subtopmet 11506  reconnlem1 11507  neibastop2lem3 11582  neibastop3 11585  topjoin 11588  fnemeet2 11590  fnejoin1 11591  fgfil 11638  supfil 11645  filssufil 11656  uffixfr 11660  ufilen 11664  limfilcf 11683  rnelfmlem 11698  fmfnfm 11704  fcluscf 11724  fcluscomplem 11732  filnetlem3 11765  filnetlem5 11767  ssga 11777  upxp 11822  upixp 11823  fimax 11837  indexd 11846  filbcmb 11857  sdc 11877  incsequz 11879  metf1o 11907  blssp 11908  metsstop 11909  mettrifi2 11913  geomcau 11914  caushft 11916  iccsplit 11919  iccshftr 11922  iccshftl 11924  iccdil 11926  icccntr 11928  icoopnst 11940  lincmb01cmp 11942  lincmb01icc 11943  cnss 11953  tlmconst 11968  txbas 11973  tx2cn 11977  txcn 11979  sstotbnd 11992  totbndss 11993  bndss 11998  totbndbnd 12000  ismtycnv 12005  ismtyhmeolem 12006  ismtyhmeo 12007  ismtybndlem 12008  ismtyres 12010  heiborlem16 12026  heiborlem23 12033  heiborlem32 12042  heiborlem34 12044  heiborlem36 12046  rrnmet 12072  rrndstprj 12073  rrncms 12075  rrntotbndlem1 12076  rrntotbndlem2 12077  rrntotbnd 12078  iccbnd 12082  phtpycolem5 12097  phtpyco 12098

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 145  df-an 223

Copyright terms: Public domain