Theorem adantll 394

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 390	. 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 410  ad2ant2lr 412  3ad2antl3 813  3adant1l 854  ax11eq 1365  ax11el 1366  reu3 1934  tz7.7 2979  limsssuc 3127  ssimaex 3774  eqfnfv 3803  dffo4 3826  fopab2 3829  fconst2g 3851  isotr 3903  isotrALT 3904  curry1 4104  oe0 4167  oesuc 4172  oecl 4178  oaordi 4186  oawordri 4190  oaass 4201  omordi 4203  omword2 4211  omlimcl 4215  odi 4216  omass 4217  nneob 4261  omsmolem 4262  dom2d 4410  sbthlem9 4461  enen1 4483  sdomen1 4487  sdomen2 4488  mapenlem2 4496  mapxpen 4501  xpmapenlem3 4504  xpmapenlem4 4505  php3 4521  php3OLD 4522  onomeneq 4525  finsucdom 4532  finsucdomOLD 4533  fiint 4572  fiintOLD 4573  fodomfi 4575  fodomfiOLD 4576  supmo 4585  ac6lem 4764  zorn2lem6 4803  axrepnd 4958  axpowndlem2 4962  axpowndlem4 4964  axinfndlem1 4969  axinfnd 4970  axacndlem4 4974  axacndlem5 4975  axacnd 4976  ltexpq 5092  ltrpq 5097  prcdpq 5109  addclprlem2 5131  prlem934b 5150  ltexpri 5161  prlem936b 5166  ssgt0sr 5229  cnegext 5360  1re 5447  axsup 5519  xrlttrt 5565  ltleaddt 5657  divadddivt 5786  divdivdivt 5787  ltdiv23t 5894  lediv23t 5895  lediv12it 5898  nn2get 5944  infmrcl 6071  xrsupsslem 6078  xrinfmsslem 6079  supxrunb1 6091  supxrunb2 6092  zextlet 6191  iooint 6373  elioc2t 6391  elico2t 6392  elicc2t 6393  elfz2nn0t 6496  fzaddelt 6501  fzrevt 6512  fzrevralt 6520  fsequb2 6525  mulexpt 6595  expaddt 6597  expmult 6598  divexpt 6600  expmwordit 6607  expnbndt 6655  sqr2irrlem3 6727  seq1ublem 6911  cau2 6913  caubnd 6926  fsum1ps 7018  fsumrev 7029  fsumshft 7031  fsumshftm 7032  fsummulc1 7033  fsumdivc 7035  fsumdivcALT 7036  fsum2mul 7037  climshft 7104  climaddlem3 7116  climaddc2 7119  climmullem4 7123  climmullem5 7124  climmullem8 7127  climsub 7130  climsup 7155  climcau 7156  caucvglem5 7161  caucvglem6 7162  caucvg 7163  cvgcmp3c 7186  cvgratlem1 7250  fsum0diag4 7261  acdc3lem 7487  acdc2lem1 7489  acdc5lem1 7492  acdclem 7495  unbenlem 7505  infpnlem1 7507  ruclem13 7523  infxpidmlem1 7553  infxpidmlem11 7563  infxpidmlem12 7564  tgss2t 7636  elcls 7701  cnconst 7777  metxp 7831  metcnplem 7883  metcnp2 7885  metcnss 7895  metcnss2 7896  tgioolem 7911  lmconst 7931  lmnn 7932  iscaunns 7941  metcnp4lem2 7966  metcnp4 7967  xplmi 7970  xpcn 7973  bopcnlem2 7979  iscms2lem3 7988  iscms2lem5 7990  bcthlem2 7997  bcthlem26 8021  bcthlem29 8024  grpidinvlem3 8047  grpidinv 8049  grpideu 8050  isgrp2i 8072  va1cnlem 8341  sm1cnilem 8343  nmoub3i 8432  nmlno0lem 8449  nmlnoubi 8452  blocnilem 8460  blocni 8461  ipasslem3 8488  ipblnfi 8512  ubthlem5 8529  ubthlem12 8536  spwpr2 8654  hvaddsub4t 8940  chocuni 9167  occllem6 9173  shsel3t 9274  chj4t 9453  spansncol 9486  5oalem2 9595  3oalem2 9603  adjsymt 9754  cnvadj 9811  nmopub2tALT 9828  unoplint 9839  counopt 9840  nmfnleub2t 9845  hmoplint 9861  brafnmult 9870  nmlnop0ALT 9915  nmopunt 9934  nmcopexlem6 9951  lnopcon 9958  nmcfnexlem6 9980  lnfncon 9985  nlelch 9989  riesz3 9990  riesz1t 9993  cnlnadjlem2 9996  cnlnadjlem6 10000  adjmult 10020  adjaddt 10021  bra11 10036  cnvbravalt 10038  kbass5t 10048  kbass6t 10049  leop2t 10052  leopaddt 10060  leopmulit 10061  leoptrit 10064  leopnmidt 10066  nmopleidt 10067  pj3s 10130  hstel2t 10141  cvcon3t 10206  dmdmdt 10222  dmdbr5 10230  mdsl0 10232  mdslmd1lem1 10247  mdslmd1lem2 10248  mdslmd3 10254  superpos 10276  irredlem2 10313  irredlem3 10314  mdsymlem3 10327  mdsymlem5 10329  mdsymlem6 10330  sumdmdlem 10340  cdjreu 10354  cdj1 10355  cdj3 10363  cdrci 10480  fgsb 10555  fgsb2 10560

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