Theorem adantll 401

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 380	. . 3 |- (ph -> (ps -> ch))
3	2	adantl 397	. 2 |- ((th /\ ph) -> (ps -> ch))
4	3	imp 357	1 |- (((th /\ ph) /\ ps) -> ch)

Syntax hints:   -> wi 3   /\ wa 230

This theorem is referenced by:  ad2ant2l 417  ad2ant2lr 419  3ad2antl3 823  3adant1l 864  ax11eq 1405  ax11el 1406  reu3 1978  tz7.7 3030  limsssuc 3178  ssimaex 3825  eqfnfv 3854  dffo4 3877  fopab2 3880  fconst2g 3902  isotr 3955  isotrALT 3956  curry1 4156  oe0 4219  oesuc 4224  oecl 4230  oaordi 4238  oawordri 4242  oaass 4253  omordi 4255  omword2 4263  omlimcl 4267  odi 4268  omass 4269  nneob 4313  omsmolem 4314  dom2d 4465  sbthlem9 4518  enen1 4540  sdomen1 4544  sdomen2 4545  mapenlem2 4555  mapxpen 4560  xpmapenlem3 4563  xpmapenlem4 4564  php3 4580  onomeneq 4583  finsucdom 4591  fiint 4620  fodomfi 4626  fodomfib 4627  supmo 4636  ac6lem 4816  zorn2lem6 4855  axrepnd 5011  axpowndlem2 5015  axpowndlem4 5017  axinfndlem1 5022  axinfnd 5023  axacndlem4 5027  axacndlem5 5028  axacnd 5029  ltexpq 5145  ltrpq 5150  prcdpq 5162  addclprlem2 5184  prlem934b 5203  ltexpri 5214  prlem936b 5219  ssgt0sr 5282  cnegex 5413  1re 5500  axsup 5572  xrlttr 5618  ltleadd 5710  divadddiv 5842  divdivdiv 5843  ltdiv23 5952  lediv23 5953  lediv12a 5956  nn2ge 6002  infmrcl 6151  xrsupsslem 6158  xrinfmsslem 6159  supxrunb1 6171  supxrunb2 6172  zextle 6274  modadd1 6380  iooin 6397  elioc2 6415  elico2 6416  elicc2 6417  elfz2nn0 6521  fzaddel 6526  fzrev 6537  fzrevral 6545  fsequb2 6550  mulexp 6683  expadd 6685  expmul 6686  divexp 6688  expmwordi 6695  expnbnd 6743  sqr2irrlem3 6816  seq1ublem 7001  cau2i 7003  caubndi 7016  fsum1ps 7108  fsumrev 7119  fsumshf 7121  fsumshftm 7122  fsummulc1 7123  fsumdivc 7125  fsumdivcALT 7126  fsum2mul 7127  climshfti 7194  climaddlem3 7206  climaddc2 7209  climmullem4 7213  climmullem5 7214  climmullem8 7217  climsub 7220  climsupi 7245  climcaui 7246  caucvglem5 7251  caucvglem6 7252  caucvgi 7253  cvgcmp3ci 7276  cvgratlem1 7340  fsum0diag4 7351  acdc3lem 7578  acdc2lem1 7580  acdc5lem1 7583  acdclem 7586  unbenlem 7596  infpnlem1 7598  ruclem13 7614  infxpidmlem1 7644  infxpidmlem11 7654  infxpidmlem12 7655  tgss2 7726  elcls 7789  cnconst 7865  metxp 7919  metcnplem 7971  metcnp2 7973  metcnss 7983  metcnss2 7984  tgioolem 7999  lmconst 8019  lmnn 8020  iscaunns 8029  metcnp4lem2 8054  metcnp4 8055  xplmi 8058  xpcn 8061  bopcnlem2 8067  iscms2lem3 8076  iscms2lem5 8078  bcthlem2 8085  bcthlem26 8109  bcthlem29 8112  grpidinvlem3 8135  grpidinv 8137  grpideu 8138  isgrp2i 8160  va1cnlem 8429  sm1cnilem 8431  nmoub3i 8520  nmlno0lem 8537  nmlnoubi 8540  blocnilem 8548  blocni 8549  ipasslem3 8576  ipblnfi 8600  ubthlem5 8617  ubthlem12 8624  spwpr2 8742  hvaddsub4 9028  chocunii 9255  occllem6 9261  shsel3 9362  chj4 9541  spansncol 9574  5oalem2 9683  3oalem2 9691  adjsym 9842  cnvadj 9899  nmopub2tALT 9916  unoplin 9927  counop 9928  nmfnleub2 9933  hmoplin 9949  brafnmul 9958  nmlnop0iALT 10003  nmopun 10022  nmcopexlem6 10039  lnopconi 10046  nmcfnexlem6 10068  lnfnconi 10073  nlelchi 10077  riesz3i 10078  riesz1 10081  cnlnadjlem2 10084  cnlnadjlem6 10088  adjmul 10108  adjadd 10109  bra11 10124  cnvbraval 10126  kbass5 10136  kbass6 10137  leop2 10140  leopadd 10148  leopmuli 10149  leoptri 10152  leopnmid 10154  nmopleid 10155  pj3si 10219  hstel2 10230  cvcon3 10295  dmdmd 10311  dmdbr5 10319  mdsl0 10321  mdslmd1lem1 10336  mdslmd1lem2 10337  mdslmd3i 10343  superpos 10365  irredlem2 10402  irredlem3 10403  mdsymlem3 10416  mdsymlem5 10418  mdsymlem6 10419  sumdmdlem 10429  cdjreui 10443  cdj1i 10444  cdj3i 10452  cdrci 10588  fgsb 10663  fgsb2 10668

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 154  df-an 232

Copyright terms: Public domain