Theorem ad2antll 727

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antll	⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Proof of Theorem ad2antll

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantl 484	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 484	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 398

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

This theorem depends on definitions:  df-bi 209  df-an 399

This theorem is referenced by:  simprr  771  simprrl  779  simprrr  780  simprr1  1217  simprr2  1218  simprr3  1219  prneimg  4778  fr2nr  5527  wereu2  5546  f1oprg  6653  fvtp1g  6954  funfvima3  6992  isof1oidb  7071  isomin  7084  weniso  7101  elovmpt3rab1  7399  sorpssi  7449  suppofssd  7861  tfrlem9a  8016  oalimcl  8180  odi  8199  oeeui  8222  ralxpmap  8454  boxriin  8498  domdifsn  8594  domunsncan  8611  enfixsn  8620  disjen  8668  mapen  8675  mapxpen  8677  mapunen  8680  unxpdomlem2  8717  unxpdomlem3  8718  findcard2d  8754  findcard3  8755  isfinite2  8770  marypha1lem  8891  marypha2  8897  supmo  8910  infmo  8953  card2inf  9013  brwdom2  9031  wemapwe  9154  rankonidlem  9251  rankxplim3  9304  djulf1o  9335  djurf1o  9336  infxpenlem  9433  infxpenc2lem1  9439  infxpenc2  9442  fseqenlem1  9444  fseqenlem2  9445  infpwfien  9482  dfac12lem2  9564  infunsdom1  9629  infunsdom  9630  infmap2  9634  fin2i2  9734  fin23lem28  9756  fin23lem32  9760  fin23lem34  9762  fin23lem40  9767  isf32lem2  9770  compssiso  9790  isfin1-3  9802  fin1a2lem10  9825  fin12  9829  hsmexlem4  9845  ac6num  9895  ttukeylem7  9931  axdclem2  9936  iundom2g  9956  fpwwe2lem12  10057  pwfseqlem3  10076  winalim2  10112  winafp  10113  wunex2  10154  grur1  10236  dedekindle  10798  00id  10809  receu  11279  lt2mul2div  11512  peano5uzi  12065  uzwo  12305  qbtwnre  12586  iooshf  12809  modmul1  13286  seqcl2  13382  seqfveq2  13386  seqid2  13410  seqdistr  13415  expcl2lem  13435  mulexpz  13463  expnlbnd2  13589  hashfun  13792  hashfacen  13806  hashf1lem1  13807  elss2prb  13839  fstwrdne0  13902  swrdsb0eq  14019  swrdswrd  14061  wrd2ind  14079  swrdccatin1  14081  pfxccatin12  14089  splid  14109  repswrevw  14143  cshwidxmod  14159  cshwidx0  14162  2cshw  14169  cshweqrep  14177  cshw1  14178  wwlktovfo  14316  relexpfld  14402  relexpindlem  14416  sqrlem6  14601  absexpz  14659  o1rlimmul  14969  iseralt  15035  summolem2  15067  fsumf1o  15074  fsum0diag2  15132  fsummulc2  15133  cvgcmpce  15167  incexclem  15185  prodmolem2  15283  fprodcl2lem  15298  fprodmul  15308  fprodrev  15325  moddvds  15612  dvdsflip  15661  bitsf1ocnv  15787  sadcaddlem  15800  bezoutlem2  15882  bezoutlem4  15884  dfgcd2  15888  lcmgcdlem  15944  crth  16109  hashgcdlem  16119  phisum  16121  pcqcl  16187  pcid  16203  pcneg  16204  prmpwdvds  16234  pockthg  16236  4sqlem11  16285  ramub2  16344  0ram  16350  prmgaplem7  16387  prmgaplem8  16388  setscom  16521  qusval  16809  initoeu1  17265  termoeu1  17272  setcinv  17344  funcestrcsetclem9  17392  funcsetcestrclem9  17407  fullsetcestrc  17410  1stfcl  17441  2ndfcl  17442  hofpropd  17511  isacs3lem  17770  frmdss2  18022  frmdup1  18023  mgm2nsgrplem2  18078  mulgdirlem  18252  mulgass  18258  0nsg  18315  cycsubgcl  18343  ghmmulg  18364  conjghm  18383  qusghm  18389  gsumwrev  18488  symg2bas  18515  symgfixelsi  18557  f1otrspeq  18569  psgnunilem2  18617  psgnunilem3  18618  odf1o2  18692  lsmhash  18825  efgtf  18842  efginvrel2  18847  efgredeu  18872  efgcpbllemb  18875  frgpuplem  18892  frgpup1  18895  cygablOLD  19005  ghmcyg  19010  gsumval3lem1  19019  gsumzres  19023  gsumzcl2  19024  gsumzf1o  19026  gsumzaddlem  19035  gsumconst  19048  gsumzmhm  19051  gsumzoppg  19058  gsum2d  19086  subgdmdprd  19150  pgpfac1lem3  19193  gsummgp0  19352  islmodd  19634  lmodvsmmulgdi  19663  islss3  19725  0lmhm  19806  idlmhm  19807  lmhmeql  19821  pwssplit3  19827  lidldvgen  20022  evlslem1  20289  coe1tmmul2  20438  pf1ind  20512  qsssubdrg  20598  cnsubrg  20599  znf1o  20692  psgnghm  20718  psgndif  20740  cssmre  20831  dsmmsubg  20881  frlmup1  20936  lindfrn  20959  f1lindf  20960  mamufval  20990  mamurid  21045  mvmulfval  21145  mdetralt2  21212  mndifsplit  21239  maducoeval2  21243  madugsum  21246  mat2pmatmul  21333  decpmatmul  21374  pm2mpf1lem  21396  pm2mpf1  21401  monmat2matmon  21426  chpscmat  21444  fvmptnn04if  21451  tgcl  21571  ppttop  21609  epttop  21611  clsval2  21652  opncldf1  21686  mretopd  21694  neindisj  21719  neiptopnei  21734  restcls  21783  restntr  21784  ordtbas  21794  cnpnei  21866  cncls2  21875  tgcmp  22003  cmpcld  22004  uncmp  22005  hauscmplem  22008  1stcfb  22047  2ndcctbss  22057  hauspwdom  22103  reftr  22116  comppfsc  22134  kgentopon  22140  ptpjpre1  22173  ptcnplem  22223  txcn  22228  txdis1cn  22237  txhaus  22249  xkopt  22257  imasnopn  22292  imasncld  22293  imasncls  22294  hmeoimaf1o  22372  cmphaushmeo  22402  txhmeo  22405  trfbas2  22445  fbasfip  22470  fbasrn  22486  fmss  22548  elfm2  22550  hauspwpwf1  22589  flfcnp  22606  fclscf  22627  flimfnfcls  22630  fcfval  22635  alexsubALTlem2  22650  alexsubALTlem3  22651  alexsubALTlem4  22652  ptcmplem3  22656  ptcmplem4  22657  cnextfval  22664  cnextcn  22669  tmdgsum2  22698  ustex2sym  22819  neipcfilu  22899  imasdsf1olem  22977  metss2lem  23115  stdbdxmet  23119  stdbdmopn  23122  metrest  23128  metcnp  23145  restmetu  23174  tngngp  23257  icccmplem1  23424  icccvx  23548  evth  23557  lebnumlem1  23559  pi1blem  23637  isncvsngp  23747  equivcau  23897  bcthlem5  23925  cmslssbn  23969  ivthlem3  24048  ovolicc2lem3  24114  ovolicc2lem4  24115  dyaddisj  24191  dyadmbllem  24194  ismbfd  24234  itg2seq  24337  itgss  24406  limciun  24486  dvcobr  24537  dvmptfsum  24566  c1liplem1  24587  c1lip1  24588  lhop  24607  dvcvx  24611  plyco0  24776  elply2  24780  plypf1  24796  dgreq0  24849  elqaalem2  24903  aalioulem6  24920  aaliou  24921  aaliou2b  24924  ulmss  24979  ulmcn  24981  pserulm  25004  lgamgulmlem5  25604  basellem4  25655  fsumdvdsdiaglem  25754  dvdsmulf1o  25765  chtublem  25781  fsumvma2  25784  logfaclbnd  25792  dchrelbasd  25809  lgsqrlem2  25917  gausslemma2dlem1a  25935  lgseisenlem2  25946  lgsquadlem1  25950  lgsquadlem2  25951  lgsquadlem3  25952  rplogsumlem2  26055  rpvmasumlem  26057  dchrmusum2  26064  dchrvmasumlem1  26065  dchrvmasum2lem  26066  rpvmasum2  26082  dchrisum0lem1  26086  logsqvma  26112  selberg4  26131  pntibndlem3  26162  pntlem3  26179  ostthlem1  26197  ostthlem2  26198  idmot  26317  brcgr  26680  brbtwn2  26685  axsegconlem8  26704  axpaschlem  26720  axeuclid  26743  axcontlem2  26745  axcontlem7  26750  eengtrkg  26766  upgrex  26871  subgrprop3  27052  subupgr  27063  nbgr0vtxlem  27131  nb3grprlem1  27156  cusgredg  27200  cusgrres  27224  usgredgsscusgredg  27235  finsumvtxdg2ssteplem4  27324  finsumvtxdg2sstep  27325  wlkl1loop  27413  wlkp1lem4  27452  wwlksnred  27664  wwlksnext  27665  wwlksnextwrd  27669  wpthswwlks2on  27734  clwwlknp  27809  clwwlkel  27819  wwlksext2clwwlk  27830  clwwlknonwwlknonb  27879  3wlkond  27944  1conngr  27967  eucrctshift  28016  fusgr2wsp2nb  28107  numclwwlk1lem2foa  28127  numclwwlk1lem2f1  28130  numclwlk1lem1  28142  numclwlk1lem2  28143  grpoidinvlem1  28275  grporcan  28289  ipblnfi  28626  hvmulcan2  28844  shscli  29088  spansneleq  29341  pjspansn  29348  3oalem2  29434  eigposi  29607  cnlnadjlem2  29839  stlesi  30012  mdslmd1lem1  30096  mdslmd1lem2  30097  cdj1i  30204  disjxpin  30332  nn0xmulclb  30490  xreceu  30593  txomap  31093  pstmxmet  31132  qqhghm  31224  qqhrhm  31225  measinblem  31474  cntmeas  31480  ballotlemsf1o  31766  bnj945  32040  bnj1110  32249  f1resveqaeq  32353  cvmopnlem  32520  cvmfolem  32521  cvmliftmolem2  32524  cvmlift2lem10  32554  satf00  32616  satffunlem2lem1  32646  satefvfmla0  32660  mrsubvrs  32764  poseq  33090  wzel  33106  sltres  33164  sslttr  33263  btwnconn1lem8  33550  btwnconn1lem9  33551  btwnconn1lem10  33552  btwnconn1lem11  33553  btwnconn1lem12  33554  finminlem  33661  nn0prpwlem  33665  fnessref  33700  refssfne  33701  fnemeet2  33710  consym1  33763  bj-finsumval0  34561  topdifinffinlem  34622  relowlssretop  34638  rdgeqoa  34645  fvineqsneu  34686  pibt2  34692  matunitlindflem1  34882  poimirlem28  34914  mblfinlem1  34923  mblfinlem3  34925  mblfinlem4  34926  ovoliunnfl  34928  mbfresfi  34932  mbfposadd  34933  itg2addnclem2  34938  itg2addnc  34940  ftc1anc  34969  frinfm  35004  fdc  35014  blssp  35025  sstotbnd  35047  isbnd2  35055  ssbnd  35060  prdstotbnd  35066  prdsbnd2  35067  ismtyres  35080  heibor1lem  35081  rrnequiv  35107  rngoisocnv  35253  crngohomfo  35278  pridlc3  35345  prter3  36012  ax12eq  36071  ax12el  36072  cvratlem  36551  islvol2aN  36722  4atlem4b  36730  4atlem4c  36731  4atlem4d  36732  isline2  36904  isline3  36906  pclfinclN  37080  linepsubclN  37081  pexmidlem4N  37103  diaglbN  38185  dvhvaddcl  38225  dvhvaddcomN  38226  dvhvscacl  38233  djavalN  38265  dibglbN  38296  dihatexv  38468  djhval  38528  mapdrvallem2  38775  prjsprellsp  39254  elrfi  39284  nacsfix  39302  eldioph2  39352  lzenom  39360  rexrabdioph  39384  irrapxlem3  39414  pellexlem5  39423  pellex  39425  pell1234qrne0  39443  pell1234qrmulcl  39445  pell14qrdich  39459  pell1qrge1  39460  pellqrex  39469  rmxypairf1o  39501  rmxycomplete  39507  monotoddzzfi  39532  congadd  39556  jm2.19lem3  39581  jm2.19lem4  39582  jm2.25  39589  jm2.26a  39590  jm2.26lem3  39591  expdiophlem1  39611  wepwsolem  39635  lmhmfgsplit  39679  aaitgo  39755  mon1psubm  39799  deg1mhm  39800  iunrelexp0  40040  isotone2  40392  mnuprdlem4  40604  disjrnmpt2  41442  mullimc  41890  mullimcf  41897  climxrre  42024  fprodcncf  42177  stoweidlem17  42296  stoweidlem27  42306  stoweidlem54  42333  fourierdlem42  42428  fourierdlem62  42447  fourierdlem73  42458  fourierdlem76  42461  fourierdlem97  42482  sge0iunmptlemfi  42689  isomenndlem  42806  ovnsslelem  42836  imarnf1pr  43475  smonoord  43525  fvelsetpreimafv  43541  iccpartiltu  43576  sprsymrelf1lem  43647  prproropf1olem3  43661  paireqne  43667  fmtnoprmfac1  43721  prmdvdsfmtnof1lem2  43741  isomushgr  43985  isomuspgrlem2c  43989  mgmhmlin  44047  rnghmmul  44165  rngcinv  44246  rngcinvALTV  44258  ringcinv  44297  funcringcsetcALTV2lem9  44309  ringcinvALTV  44321  funcringcsetclem9ALTV  44332  mndpsuppss  44413  lmodvsmdi  44424  lincsum  44478  lindslinindimp2lem4  44510  nn0sumshdiglemB  44674