Theorem ad2antll 729

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 485	. 2 ⊢ ((𝜃 ∧ 𝜑) → 𝜓)
3	2	adantl 485	1 ⊢ ((𝜒 ∧ (𝜃 ∧ 𝜑)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simprr  773  simprrl  781  simprrr  782  simprr1  1223  simprr2  1224  simprr3  1225  prneimg  4765  fr2nr  5529  wereu2  5548  f1oprg  6705  fvtp1g  7013  funfvima3  7052  isof1oidb  7133  isomin  7146  weniso  7163  elovmpt3rab1  7465  sorpssi  7517  suppofssd  7945  tfrlem9a  8122  oalimcl  8288  odi  8307  oeeui  8330  ralxpmap  8577  boxriin  8621  domdifsn  8728  domunsncan  8745  enfixsn  8754  disjen  8803  mapen  8810  mapxpen  8812  mapunen  8815  findcard2d  8844  unxpdomlem2  8883  unxpdomlem3  8884  findcard3  8914  isfinite2  8929  marypha1lem  9049  marypha2  9055  supmo  9068  infmo  9111  card2inf  9171  brwdom2  9189  wemapwe  9312  rankonidlem  9444  rankxplim3  9497  djulf1o  9528  djurf1o  9529  infxpenlem  9627  infxpenc2lem1  9633  infxpenc2  9636  fseqenlem1  9638  fseqenlem2  9639  infpwfien  9676  dfac12lem2  9758  infunsdom1  9827  infunsdom  9828  infmap2  9832  fin2i2  9932  fin23lem28  9954  fin23lem32  9958  fin23lem34  9960  fin23lem40  9965  isf32lem2  9968  compssiso  9988  isfin1-3  10000  fin1a2lem10  10023  fin12  10027  hsmexlem4  10043  ac6num  10093  ttukeylem7  10129  axdclem2  10134  iundom2g  10154  fpwwe2lem11  10255  pwfseqlem3  10274  winalim2  10310  winafp  10311  wunex2  10352  grur1  10434  dedekindle  10996  00id  11007  receu  11477  lt2mul2div  11710  peano5uzi  12266  uzwo  12507  qbtwnre  12789  iooshf  13014  modmul1  13497  seqcl2  13594  seqfveq2  13598  seqid2  13622  seqdistr  13627  expcl2lem  13647  mulexpz  13675  expnlbnd2  13801  hashfun  14004  hashfacen  14018  hashfacenOLD  14019  hashf1lem1  14020  hashf1lem1OLD  14021  elss2prb  14053  fstwrdne0  14111  swrdsb0eq  14228  swrdswrd  14270  wrd2ind  14288  swrdccatin1  14290  pfxccatin12  14298  splid  14318  repswrevw  14352  cshwidxmod  14368  cshwidx0  14371  2cshw  14378  cshweqrep  14386  cshw1  14387  wwlktovfo  14525  relexpfld  14612  relexpindlem  14626  sqrlem6  14811  absexpz  14869  o1rlimmul  15180  iseralt  15248  summolem2  15280  fsumf1o  15287  fsum0diag2  15347  fsummulc2  15348  cvgcmpce  15382  incexclem  15400  prodmolem2  15497  fprodcl2lem  15512  fprodmul  15522  fprodrev  15539  moddvds  15826  dvdsflip  15878  bitsf1ocnv  16003  sadcaddlem  16016  bezoutlem2  16100  bezoutlem4  16102  dfgcd2  16106  lcmgcdlem  16163  crth  16331  hashgcdlem  16341  phisum  16343  pcqcl  16409  pcid  16426  pcneg  16427  prmpwdvds  16457  pockthg  16459  4sqlem11  16508  ramub2  16567  0ram  16573  prmgaplem7  16610  prmgaplem8  16611  setscom  16733  qusval  17047  initoeu1  17517  termoeu1  17524  setcinv  17596  funcestrcsetclem9  17655  funcsetcestrclem9  17670  fullsetcestrc  17673  1stfcl  17704  2ndfcl  17705  hofpropd  17775  isacs3lem  18048  frmdss2  18290  frmdup1  18291  mgm2nsgrplem2  18346  mulgdirlem  18522  mulgass  18528  0nsg  18585  cycsubgcl  18613  ghmmulg  18634  conjghm  18653  qusghm  18659  gsumwrev  18758  symg2bas  18785  symgfixelsi  18827  f1otrspeq  18839  psgnunilem2  18887  psgnunilem3  18888  odf1o2  18962  lsmhash  19095  efgtf  19112  efginvrel2  19117  efgredeu  19142  efgcpbllemb  19145  frgpuplem  19162  frgpup1  19165  cygablOLD  19276  ghmcyg  19281  gsumval3lem1  19290  gsumzres  19294  gsumzcl2  19295  gsumzf1o  19297  gsumzaddlem  19306  gsumconst  19319  gsumzmhm  19322  gsumzoppg  19329  gsum2d  19357  subgdmdprd  19421  pgpfac1lem3  19464  gsummgp0  19626  islmodd  19905  lmodvsmmulgdi  19934  islss3  19996  0lmhm  20077  idlmhm  20078  lmhmeql  20092  pwssplit3  20098  lidldvgen  20293  qsssubdrg  20422  cnsubrg  20423  znf1o  20516  psgnghm  20542  psgndif  20564  cssmre  20655  dsmmsubg  20705  frlmup1  20760  lindfrn  20783  f1lindf  20784  evlslem1  21042  coe1tmmul2  21197  pf1ind  21271  mamufval  21284  mamurid  21339  mvmulfval  21439  mdetralt2  21506  mndifsplit  21533  maducoeval2  21537  madugsum  21540  mat2pmatmul  21628  decpmatmul  21669  pm2mpf1lem  21691  pm2mpf1  21696  monmat2matmon  21721  chpscmat  21739  fvmptnn04if  21746  tgcl  21866  ppttop  21904  epttop  21906  clsval2  21947  opncldf1  21981  mretopd  21989  neindisj  22014  neiptopnei  22029  restcls  22078  restntr  22079  ordtbas  22089  cnpnei  22161  cncls2  22170  tgcmp  22298  cmpcld  22299  uncmp  22300  hauscmplem  22303  1stcfb  22342  2ndcctbss  22352  hauspwdom  22398  reftr  22411  comppfsc  22429  kgentopon  22435  ptpjpre1  22468  ptcnplem  22518  txcn  22523  txdis1cn  22532  txhaus  22544  xkopt  22552  imasnopn  22587  imasncld  22588  imasncls  22589  hmeoimaf1o  22667  cmphaushmeo  22697  txhmeo  22700  trfbas2  22740  fbasfip  22765  fbasrn  22781  fmss  22843  elfm2  22845  hauspwpwf1  22884  flfcnp  22901  fclscf  22922  flimfnfcls  22925  fcfval  22930  alexsubALTlem2  22945  alexsubALTlem3  22946  alexsubALTlem4  22947  ptcmplem3  22951  ptcmplem4  22952  cnextfval  22959  cnextcn  22964  tmdgsum2  22993  ustex2sym  23114  neipcfilu  23193  imasdsf1olem  23271  metss2lem  23409  stdbdxmet  23413  stdbdmopn  23416  metrest  23422  metcnp  23439  restmetu  23468  tngngp  23552  icccmplem1  23719  icccvx  23847  evth  23856  lebnumlem1  23858  pi1blem  23936  isncvsngp  24046  equivcau  24197  bcthlem5  24225  cmslssbn  24269  ivthlem3  24350  ovolicc2lem3  24416  ovolicc2lem4  24417  dyaddisj  24493  dyadmbllem  24496  ismbfd  24536  itg2seq  24640  itgss  24709  limciun  24791  dvcobr  24843  dvmptfsum  24872  c1liplem1  24893  c1lip1  24894  lhop  24913  dvcvx  24917  tdeglem4  24957  plyco0  25086  elply2  25090  plypf1  25106  dgreq0  25159  elqaalem2  25213  aalioulem6  25230  aaliou  25231  aaliou2b  25234  ulmss  25289  ulmcn  25291  pserulm  25314  lgamgulmlem5  25915  basellem4  25966  fsumdvdsdiaglem  26065  dvdsmulf1o  26076  chtublem  26092  fsumvma2  26095  logfaclbnd  26103  dchrelbasd  26120  lgsqrlem2  26228  gausslemma2dlem1a  26246  lgseisenlem2  26257  lgsquadlem1  26261  lgsquadlem2  26262  lgsquadlem3  26263  rplogsumlem2  26366  rpvmasumlem  26368  dchrmusum2  26375  dchrvmasumlem1  26376  dchrvmasum2lem  26377  rpvmasum2  26393  dchrisum0lem1  26397  logsqvma  26423  selberg4  26442  pntibndlem3  26473  pntlem3  26490  ostthlem1  26508  ostthlem2  26509  idmot  26628  brcgr  26991  brbtwn2  26996  axsegconlem8  27015  axpaschlem  27031  axeuclid  27054  axcontlem2  27056  axcontlem7  27061  eengtrkg  27077  upgrex  27183  subgrprop3  27364  subupgr  27375  nbgr0vtxlem  27443  nb3grprlem1  27468  cusgredg  27512  cusgrres  27536  usgredgsscusgredg  27547  finsumvtxdg2ssteplem4  27636  finsumvtxdg2sstep  27637  wlkl1loop  27725  wlkp1lem4  27764  wwlksnred  27976  wwlksnext  27977  wwlksnextwrd  27981  wpthswwlks2on  28045  clwwlknp  28120  clwwlkel  28129  wwlksext2clwwlk  28140  clwwlknonwwlknonb  28189  3wlkond  28254  1conngr  28277  eucrctshift  28326  fusgr2wsp2nb  28417  numclwwlk1lem2foa  28437  numclwwlk1lem2f1  28440  numclwlk1lem1  28452  numclwlk1lem2  28453  grpoidinvlem1  28585  grporcan  28599  ipblnfi  28936  hvmulcan2  29154  shscli  29398  spansneleq  29651  pjspansn  29658  3oalem2  29744  eigposi  29917  cnlnadjlem2  30149  stlesi  30322  mdslmd1lem1  30406  mdslmd1lem2  30407  cdj1i  30514  disjxpin  30646  nn0xmulclb  30814  xreceu  30916  txomap  31498  pstmxmet  31561  qqhghm  31650  qqhrhm  31651  measinblem  31900  cntmeas  31906  ballotlemsf1o  32192  bnj945  32466  bnj1110  32675  f1resveqaeq  32770  cvmopnlem  32953  cvmfolem  32954  cvmliftmolem2  32957  cvmlift2lem10  32987  satf00  33049  satffunlem2lem1  33079  satefvfmla0  33093  mrsubvrs  33197  poxp3  33533  poseq  33539  wzel  33555  sltres  33602  nogt01o  33636  oldbdayim  33808  btwnconn1lem8  34133  btwnconn1lem9  34134  btwnconn1lem10  34135  btwnconn1lem11  34136  btwnconn1lem12  34137  finminlem  34244  nn0prpwlem  34248  fnessref  34283  refssfne  34284  fnemeet2  34293  consym1  34346  bj-finsumval0  35191  topdifinffinlem  35255  relowlssretop  35271  rdgeqoa  35278  fvineqsneu  35319  pibt2  35325  matunitlindflem1  35510  poimirlem28  35542  mblfinlem1  35551  mblfinlem3  35553  mblfinlem4  35554  ovoliunnfl  35556  mbfresfi  35560  mbfposadd  35561  itg2addnclem2  35566  itg2addnc  35568  ftc1anc  35595  frinfm  35630  fdc  35640  blssp  35651  sstotbnd  35670  isbnd2  35678  ssbnd  35683  prdstotbnd  35689  prdsbnd2  35690  ismtyres  35703  heibor1lem  35704  rrnequiv  35730  rngoisocnv  35876  crngohomfo  35901  pridlc3  35968  prter3  36633  ax12eq  36692  ax12el  36693  cvratlem  37172  islvol2aN  37343  4atlem4b  37351  4atlem4c  37352  4atlem4d  37353  isline2  37525  isline3  37527  pclfinclN  37701  linepsubclN  37702  pexmidlem4N  37724  diaglbN  38806  dvhvaddcl  38846  dvhvaddcomN  38847  dvhvscacl  38854  djavalN  38886  dibglbN  38917  dihatexv  39089  djhval  39149  mapdrvallem2  39396  metakunt15  39861  mhpind  39993  prjsprellsp  40158  elrfi  40219  nacsfix  40237  eldioph2  40287  lzenom  40295  rexrabdioph  40319  irrapxlem3  40349  pellexlem5  40358  pellex  40360  pell1234qrne0  40378  pell1234qrmulcl  40380  pell14qrdich  40394  pell1qrge1  40395  pellqrex  40404  rmxypairf1o  40436  rmxycomplete  40442  monotoddzzfi  40467  congadd  40491  jm2.19lem3  40516  jm2.19lem4  40517  jm2.25  40524  jm2.26a  40525  jm2.26lem3  40526  expdiophlem1  40546  wepwsolem  40570  lmhmfgsplit  40614  aaitgo  40690  mon1psubm  40734  deg1mhm  40735  iunrelexp0  40987  isotone2  41336  mnuprdlem4  41566  disjrnmpt2  42399  mullimc  42832  mullimcf  42839  climxrre  42966  fprodcncf  43116  stoweidlem17  43233  stoweidlem27  43243  stoweidlem54  43270  fourierdlem42  43365  fourierdlem62  43384  fourierdlem73  43395  fourierdlem76  43398  fourierdlem97  43419  sge0iunmptlemfi  43626  isomenndlem  43743  ovnsslelem  43773  imarnf1pr  44446  smonoord  44496  fvelsetpreimafv  44512  iccpartiltu  44547  sprsymrelf1lem  44616  prproropf1olem3  44630  paireqne  44636  fmtnoprmfac1  44690  prmdvdsfmtnof1lem2  44710  isomushgr  44951  isomuspgrlem2c  44955  mgmhmlin  45013  rnghmmul  45131  rngcinv  45212  rngcinvALTV  45224  ringcinv  45263  funcringcsetcALTV2lem9  45275  ringcinvALTV  45287  funcringcsetclem9ALTV  45298  mndpsuppss  45380  lmodvsmdi  45391  lincsum  45443  lindslinindimp2lem4  45475  nn0sumshdiglemB  45639  1arymaptf1  45661  2arymaptf1  45672