Theorem adantll 309

Description: Deduction adding a conjunct to an 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	exp 291	. . 3 |- (ph -> (ps -> ch))
3	2	adantl 305	. 2 |- ((th /\ ph) -> (ps -> ch))
4	3	imp 277	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 2   /\ wa 196

This theorem is referenced by:  supmo 2156  tz7.7 2224  limsssuc 2362  fvco 2865  cleqfv 2880  fopab2 2891  isotr 2935  isotrALT 2936  caoprmo 3084  oe0 3130  oesuc 3134  oecl 3140  oaordi 3148  oawordri 3152  oaass 3163  omordi 3164  omsmolem 3195  dom2d 3307  xpdom2 3345  sbthlem9 3357  enen1 3375  sdomen1 3379  sdomen2 3380  mapenlem2 3385  mapxpen 3390  xpmapenlem3 3393  xpmapenlem4 3394  php3 3411  onomeneq 3414  finsucdom 3421  fiint 3445  ac6lem 3575  zornlem6 3608  axrepnd 3740  axpowndlem2 3744  axpowndlem4 3746  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  ordpipq 3850  ltsopq 3869  ltexpq 3874  ltrpq 3879  prcdpq 3891  addclprlem2 3913  prlem934b 3932  ltexpri 3943  prlem936b 3948  ltsrpr 3980  ltsosr 3997  ssgt0sr 4011  axrecex 4079  divmuldivt 4263  divadddivt 4264  divdivdivt 4265  zltp1let 4597  uzwo2 4606  zmax 4618  zbtwnre 4619  qaddclt 4642  expaddt 4698  sqr2irrlem3 4779  ruclem13 4897  infxpidmlem1 4933  infxpidmlem11 4943  infxpidmlem12 4944  hvsub4t 5014  chocuni 5179  occllem6 5185  spansncol 5473  osumlem3 5532  osumlem4 5533  5oalem2 5545  3oalem2 5553  pj3s 5659  cvcon3t 5716  dmdbr 5731  atcvat3 5774  mdsymlem3 5778  mdsymlem5 5780  mdsymlem6 5781  sumdmdlem 5786

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org