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 373	. . 3 |- (ph -> (ps -> ch))
3	2	adantl 388	. 2 |- ((th /\ ph) -> (ps -> ch))
4	3	imp 350	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 223

This theorem is referenced by:  ad2ant2l 408  ad2ant2lr 410  3ad2antl3 811  3adant1l 852  ax11eq 1363  ax11el 1364  reu3 1931  tz7.7 2973  limsssuc 3121  ssimaex 3768  eqfnfv 3797  dffo4 3820  fopab2 3823  fconst2g 3845  isotr 3897  isotrALT 3898  curry1 4098  oe0 4161  oesuc 4166  oecl 4172  oaordi 4180  oawordri 4184  oaass 4195  omordi 4197  omword2 4205  omlimcl 4209  odi 4210  omass 4211  nneob 4255  omsmolem 4256  dom2d 4403  sbthlem9 4453  enen1 4475  sdomen1 4479  sdomen2 4480  mapenlem2 4488  mapxpen 4493  xpmapenlem3 4496  xpmapenlem4 4497  php3 4513  onomeneq 4516  finsucdom 4524  fiint 4552  fodomfi 4558  fodomfib 4559  supmo 4568  ac6lem 4746  zorn2lem6 4785  axrepnd 4938  axpowndlem2 4942  axpowndlem4 4944  axinfndlem1 4949  axinfnd 4950  axacndlem4 4954  axacndlem5 4955  axacnd 4956  ltexpq 5072  ltrpq 5077  prcdpq 5089  addclprlem2 5111  prlem934b 5130  ltexpri 5141  prlem936b 5146  ssgt0sr 5209  cnegext 5340  1re 5427  axsup 5499  xrlttrt 5545  ltleaddt 5637  divadddivt 5772  divdivdivt 5773  ltdiv23t 5880  lediv23t 5881  lediv12it 5884  nn2get 5930  infmrcl 6057  xrsupsslem 6064  xrinfmsslem 6065  supxrunb1 6077  supxrunb2 6078  zextlet 6177  iooint 6358  elioc2t 6376  elico2t 6377  elicc2t 6378  elfz2nn0t 6481  fzaddelt 6486  fzrevt 6497  fzrevralt 6505  fsequb2 6510  mulexpt 6580  expaddt 6582  expmult 6583  divexpt 6585  expmwordit 6592  expnbndt 6640  sqr2irrlem3 6712  seq1ublem 6896  cau2 6898  caubnd 6911  fsum1ps 7003  fsumrev 7014  fsumshft 7016  fsumshftm 7017  fsummulc1 7018  fsumdivc 7020  fsumdivcALT 7021  fsum2mul 7022  climshft 7089  climaddlem3 7101  climaddc2 7104  climmullem4 7108  climmullem5 7109  climmullem8 7112  climsub 7115  climsup 7140  climcau 7141  caucvglem5 7146  caucvglem6 7147  caucvg 7148  cvgcmp3c 7171  cvgratlem1 7235  fsum0diag4 7246  acdc3lem 7471  acdc2lem1 7473  acdc5lem1 7476  acdclem 7479  unbenlem 7489  infpnlem1 7491  ruclem13 7507  infxpidmlem1 7537  infxpidmlem11 7547  infxpidmlem12 7548  tgss2t 7622  elcls 7689  cnconst 7765  metxp 7819  metcnplem 7871  metcnp2 7873  metcnss 7883  metcnss2 7884  tgioolem 7899  lmconst 7919  lmnn 7920  iscaunns 7929  metcnp4lem2 7954  metcnp4 7955  xplmi 7958  xpcn 7961  bopcnlem2 7967  iscms2lem3 7976  iscms2lem5 7978  bcthlem2 7985  bcthlem26 8009  bcthlem29 8012  grpidinvlem3 8035  grpidinv 8037  grpideu 8038  isgrp2i 8061  va1cnlem 8330  sm1cnilem 8332  nmoub3i 8421  nmlno0lem 8438  nmlnoubi 8441  blocnilem 8449  blocni 8450  ipasslem3 8477  ipblnfi 8501  ubthlem5 8518  ubthlem12 8525  spwpr2 8643  hvaddsub4t 8930  chocuni 9157  occllem6 9163  shsel3t 9264  chj4t 9443  spansncol 9476  5oalem2 9585  3oalem2 9593  adjsymt 9744  cnvadj 9801  nmopub2tALT 9818  unoplint 9829  counopt 9830  nmfnleub2t 9835  hmoplint 9851  brafnmult 9860  nmlnop0ALT 9905  nmopunt 9924  nmcopexlem6 9941  lnopcon 9948  nmcfnexlem6 9970  lnfncon 9975  nlelch 9979  riesz3 9980  riesz1t 9983  cnlnadjlem2 9986  cnlnadjlem6 9990  adjmult 10010  adjaddt 10011  bra11 10026  cnvbravalt 10028  kbass5t 10038  kbass6t 10039  leop2t 10042  leopaddt 10050  leopmulit 10051  leoptrit 10054  leopnmidt 10056  nmopleidt 10057  pj3s 10120  hstel2t 10131  cvcon3t 10196  dmdmdt 10212  dmdbr5 10220  mdsl0 10222  mdslmd1lem1 10237  mdslmd1lem2 10238  mdslmd3 10244  superpos 10266  irredlem2 10303  irredlem3 10304  mdsymlem3 10317  mdsymlem5 10319  mdsymlem6 10320  sumdmdlem 10330  cdjreu 10344  cdj1 10345  cdj3 10353  cdrci 10466  fgsb 10529  fgsb2 10535

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