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 4404  sbthlem9 4455  enen1 4477  sdomen1 4481  sdomen2 4482  mapenlem2 4490  mapxpen 4495  xpmapenlem3 4498  xpmapenlem4 4499  php3 4515  php3OLD 4516  onomeneq 4519  finsucdomOLD 4527  fiint 4559  fiintOLD 4560  fodomfiOLD 4566  fodomfibOLD 4567  supmo 4576  ac6lem 4754  zorn2lem6 4793  axrepnd 4946  axpowndlem2 4950  axpowndlem4 4952  axinfndlem1 4957  axinfnd 4958  axacndlem4 4962  axacndlem5 4963  axacnd 4964  ltexpq 5080  ltrpq 5085  prcdpq 5097  addclprlem2 5119  prlem934b 5138  ltexpri 5149  prlem936b 5154  ssgt0sr 5217  cnegext 5348  1re 5435  axsup 5507  xrlttrt 5553  ltleaddt 5645  divadddivt 5784  divdivdivt 5785  ltdiv23t 5892  lediv23t 5893  lediv12it 5896  nn2get 5942  infmrcl 6069  xrsupsslem 6076  xrinfmsslem 6077  supxrunb1 6089  supxrunb2 6090  zextlet 6189  iooint 6372  elioc2t 6390  elico2t 6391  elicc2t 6392  elfz2nn0t 6495  fzaddelt 6500  fzrevt 6511  fzrevralt 6519  fsequb2 6524  mulexpt 6594  expaddt 6596  expmult 6597  divexpt 6599  expmwordit 6606  expnbndt 6654  sqr2irrlem3 6726  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 7486  acdc2lem1 7488  acdc5lem1 7491  acdclem 7494  unbenlem 7504  infpnlem1 7506  ruclem13 7522  infxpidmlem1 7552  infxpidmlem11 7562  infxpidmlem12 7563  tgss2t 7637  elcls 7704  cnconst 7780  metxp 7834  metcnplem 7886  metcnp2 7888  metcnss 7898  metcnss2 7899  tgioolem 7914  lmconst 7934  lmnn 7935  iscaunns 7944  metcnp4lem2 7969  metcnp4 7970  xplmi 7973  xpcn 7976  bopcnlem2 7982  iscms2lem3 7991  iscms2lem5 7993  bcthlem2 8000  bcthlem26 8024  bcthlem29 8027  grpidinvlem3 8050  grpidinv 8052  grpideu 8053  isgrp2i 8076  va1cnlem 8345  sm1cnilem 8347  nmoub3i 8436  nmlno0lem 8453  nmlnoubi 8456  blocnilem 8464  blocni 8465  ipasslem3 8492  ipblnfi 8516  ubthlem5 8533  ubthlem12 8540  spwpr2 8658  hvaddsub4t 8945  chocuni 9172  occllem6 9178  shsel3t 9279  chj4t 9458  spansncol 9491  5oalem2 9600  3oalem2 9608  adjsymt 9759  cnvadj 9816  nmopub2tALT 9833  unoplint 9844  counopt 9845  nmfnleub2t 9850  hmoplint 9866  brafnmult 9875  nmlnop0ALT 9920  nmopunt 9939  nmcopexlem6 9956  lnopcon 9963  nmcfnexlem6 9985  lnfncon 9990  nlelch 9994  riesz3 9995  riesz1t 9998  cnlnadjlem2 10001  cnlnadjlem6 10005  adjmult 10025  adjaddt 10026  bra11 10041  cnvbravalt 10043  kbass5t 10053  kbass6t 10054  leop2t 10057  leopaddt 10065  leopmulit 10066  leoptrit 10069  leopnmidt 10071  nmopleidt 10072  pj3s 10135  hstel2t 10146  cvcon3t 10211  dmdmdt 10227  dmdbr5 10235  mdsl0 10237  mdslmd1lem1 10252  mdslmd1lem2 10253  mdslmd3 10259  superpos 10281  irredlem2 10318  irredlem3 10319  mdsymlem3 10332  mdsymlem5 10334  mdsymlem6 10335  sumdmdlem 10345  cdjreu 10359  cdj1 10360  cdj3 10368  cdrci 10494  fgsb 10570  fgsbOLD 10571  fgsb2 10580

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