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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprr  772  simprrl  780  simprrr  781  simprr1  1222  simprr2  1223  simprr3  1224  prneimg  4821  prproe  4872  fr2nr  5618  wereu2  5638  f1oprg  6848  fvtp1g  7175  funfvima3  7213  isof1oidb  7302  isomin  7315  weniso  7332  elovmpt3rab1  7652  sorpssi  7708  resf1extb  7913  poseq  8140  suppofssd  8185  tfrlem9a  8357  oalimcl  8527  odi  8546  oeeui  8569  ralxpmap  8872  boxriin  8916  domdifsn  9028  domunsncan  9046  enfixsn  9055  disjen  9104  mapen  9111  mapxpen  9113  mapunen  9116  findcard2d  9136  unxpdomlem2  9205  unxpdomlem3  9206  findcard3OLD  9237  isfinite2  9252  marypha1lem  9391  marypha2  9397  supmo  9410  infmo  9455  card2inf  9515  brwdom2  9533  wemapwe  9657  rankonidlem  9788  rankxplim3  9841  djulf1o  9872  djurf1o  9873  infxpenlem  9973  infxpenc2lem1  9979  infxpenc2  9982  fseqenlem1  9984  fseqenlem2  9985  infpwfien  10022  dfac12lem2  10105  infunsdom1  10172  infunsdom  10173  infmap2  10177  fin2i2  10278  fin23lem28  10300  fin23lem32  10304  fin23lem34  10306  fin23lem40  10311  isf32lem2  10314  compssiso  10334  isfin1-3  10346  fin1a2lem10  10369  fin12  10373  hsmexlem4  10389  ac6num  10439  ttukeylem7  10475  axdclem2  10480  iundom2g  10500  fpwwe2lem11  10601  pwfseqlem3  10620  winalim2  10656  winafp  10657  wunex2  10698  grur1  10780  dedekindle  11345  00id  11356  receu  11830  lt2mul2div  12068  peano5uzi  12630  uzwo  12877  qbtwnre  13166  iooshf  13394  modmul1  13896  seqcl2  13992  seqfveq2  13996  seqid2  14020  seqdistr  14025  expcl2lem  14045  mulexpz  14074  expnlbnd2  14206  hashfun  14409  hashfacen  14426  hashf1lem1  14427  elss2prb  14460  fstwrdne0  14528  swrdsb0eq  14635  swrdswrd  14677  wrd2ind  14695  swrdccatin1  14697  pfxccatin12  14705  splid  14725  repswrevw  14759  cshwidxmod  14775  cshwidx0  14778  2cshw  14785  cshweqrep  14793  cshw1  14794  wwlktovfo  14931  relexpfld  15022  relexpindlem  15036  01sqrexlem6  15220  absexpz  15278  o1rlimmul  15592  iseralt  15658  summolem2  15689  fsumf1o  15696  fsum0diag2  15756  fsummulc2  15757  cvgcmpce  15791  incexclem  15809  prodmolem2  15908  fprodcl2lem  15923  fprodmul  15933  fprodrev  15950  moddvds  16240  dvdsflip  16294  bitsf1ocnv  16421  sadcaddlem  16434  bezoutlem2  16517  bezoutlem4  16519  dfgcd2  16523  lcmgcdlem  16583  crth  16755  hashgcdlem  16765  phisum  16768  pcqcl  16834  pcid  16851  pcneg  16852  prmpwdvds  16882  pockthg  16884  4sqlem11  16933  ramub2  16992  0ram  16998  prmgaplem7  17035  prmgaplem8  17036  setscom  17157  qusval  17512  initoeu1  17980  termoeu1  17987  setcinv  18059  funcestrcsetclem9  18116  funcsetcestrclem9  18131  fullsetcestrc  18134  1stfcl  18165  2ndfcl  18166  hofpropd  18235  isacs3lem  18508  mgmhmlin  18633  mndpsuppss  18699  frmdss2  18797  frmdup1  18798  mgm2nsgrplem2  18853  mulgdirlem  19044  mulgass  19050  0nsg  19108  cycsubgcl  19145  ghmmulg  19167  conjghm  19188  qusghm  19194  gsumwrev  19305  symg2bas  19330  symgfixelsi  19372  f1otrspeq  19384  psgnunilem2  19432  psgnunilem3  19433  odf1o2  19510  lsmhash  19642  efgtf  19659  efginvrel2  19664  efgredeu  19689  efgcpbllemb  19692  frgpuplem  19709  frgpup1  19712  ghmcyg  19833  gsumval3lem1  19842  gsumzres  19846  gsumzcl2  19847  gsumzf1o  19849  gsumzaddlem  19858  gsumconst  19871  gsumzmhm  19874  gsumzoppg  19881  gsum2d  19909  subgdmdprd  19973  pgpfac1lem3  20016  gsummgp0  20234  rnghmmul  20365  rngcinv  20553  ringcinv  20587  islmodd  20779  lmodvsmmulgdi  20810  islss3  20872  0lmhm  20954  idlmhm  20955  lmhmeql  20969  pwssplit3  20975  lidldvgen  21251  qsssubdrg  21350  cnsubrg  21351  znf1o  21468  psgnghm  21496  psgndif  21518  cssmre  21609  dsmmsubg  21659  frlmup1  21714  lindfrn  21737  f1lindf  21738  evlslem1  21996  psdmul  22060  coe1tmmul2  22169  pf1ind  22249  mamufval  22286  mamurid  22336  mvmulfval  22436  mdetralt2  22503  mndifsplit  22530  maducoeval2  22534  madugsum  22537  mat2pmatmul  22625  decpmatmul  22666  pm2mpf1lem  22688  pm2mpf1  22693  monmat2matmon  22718  chpscmat  22736  fvmptnn04if  22743  tgcl  22863  ppttop  22901  epttop  22903  clsval2  22944  opncldf1  22978  mretopd  22986  neindisj  23011  neiptopnei  23026  restcls  23075  restntr  23076  ordtbas  23086  cnpnei  23158  cncls2  23167  tgcmp  23295  cmpcld  23296  uncmp  23297  hauscmplem  23300  1stcfb  23339  2ndcctbss  23349  hauspwdom  23395  reftr  23408  comppfsc  23426  kgentopon  23432  ptpjpre1  23465  ptcnplem  23515  txcn  23520  txdis1cn  23529  txhaus  23541  xkopt  23549  imasnopn  23584  imasncld  23585  imasncls  23586  hmeoimaf1o  23664  cmphaushmeo  23694  txhmeo  23697  trfbas2  23737  fbasfip  23762  fbasrn  23778  fmss  23840  elfm2  23842  hauspwpwf1  23881  flfcnp  23898  fclscf  23919  flimfnfcls  23922  fcfval  23927  alexsubALTlem2  23942  alexsubALTlem3  23943  alexsubALTlem4  23944  ptcmplem3  23948  ptcmplem4  23949  cnextfval  23956  cnextcn  23961  tmdgsum2  23990  ustex2sym  24111  neipcfilu  24190  imasdsf1olem  24268  metss2lem  24406  stdbdxmet  24410  stdbdmopn  24413  metrest  24419  metcnp  24436  restmetu  24465  tngngp  24549  icccmplem1  24718  icccvx  24855  evth  24865  lebnumlem1  24867  pi1blem  24946  isncvsngp  25056  equivcau  25207  bcthlem5  25235  cmslssbn  25279  ivthlem3  25361  ovolicc2lem3  25427  ovolicc2lem4  25428  dyaddisj  25504  dyadmbllem  25507  ismbfd  25547  itg2seq  25650  itgss  25720  limciun  25802  dvcobr  25856  dvcobrOLD  25857  dvmptfsum  25886  c1liplem1  25908  c1lip1  25909  lhop  25928  dvcvx  25932  tdeglem4  25972  plyco0  26104  elply2  26108  plypf1  26124  dgreq0  26178  elqaalem2  26235  aalioulem6  26252  aaliou  26253  aaliou2b  26256  ulmss  26313  ulmcn  26315  pserulm  26338  lgamgulmlem5  26950  basellem4  27001  fsumdvdsdiaglem  27100  mpodvdsmulf1o  27111  dvdsmulf1o  27113  chtublem  27129  fsumvma2  27132  logfaclbnd  27140  dchrelbasd  27157  lgsqrlem2  27265  gausslemma2dlem1a  27283  lgseisenlem2  27294  lgsquadlem1  27298  lgsquadlem2  27299  lgsquadlem3  27300  rplogsumlem2  27403  rpvmasumlem  27405  dchrmusum2  27412  dchrvmasumlem1  27413  dchrvmasum2lem  27414  rpvmasum2  27430  dchrisum0lem1  27434  logsqvma  27460  selberg4  27479  pntibndlem3  27510  pntlem3  27527  ostthlem1  27545  ostthlem2  27546  sltres  27581  nogt01o  27615  oldbdayim  27807  addsproplem2  27884  negsproplem2  27942  mulsval  28019  om2noseqrdg  28205  noseqrdgfn  28207  zmulscld  28292  recut  28354  idmot  28471  brcgr  28834  brbtwn2  28839  axsegconlem8  28858  axpaschlem  28874  axeuclid  28897  axcontlem2  28899  axcontlem7  28904  eengtrkg  28920  upgrex  29026  subgrprop3  29210  subupgr  29221  nbgr0edglem  29290  nb3grprlem1  29314  cusgredg  29358  cusgrres  29383  usgredgsscusgredg  29394  finsumvtxdg2ssteplem4  29483  finsumvtxdg2sstep  29484  wlkl1loop  29573  wlkp1lem4  29611  wwlksnred  29829  wwlksnext  29830  wwlksnextwrd  29834  wpthswwlks2on  29898  clwwlknp  29973  clwwlkel  29982  wwlksext2clwwlk  29993  clwwlknonwwlknonb  30042  3wlkond  30107  1conngr  30130  eucrctshift  30179  fusgr2wsp2nb  30270  numclwwlk1lem2foa  30290  numclwwlk1lem2f1  30293  numclwlk1lem1  30305  numclwlk1lem2  30306  grpoidinvlem1  30440  grporcan  30454  ipblnfi  30791  hvmulcan2  31009  shscli  31253  spansneleq  31506  pjspansn  31513  3oalem2  31599  eigposi  31772  cnlnadjlem2  32004  stlesi  32177  mdslmd1lem1  32261  mdslmd1lem2  32262  cdj1i  32369  disjxpin  32524  nn0xmulclb  32701  xreceu  32849  txomap  33831  pstmxmet  33894  qqhghm  33985  qqhrhm  33986  measinblem  34217  cntmeas  34223  ballotlemsf1o  34512  bnj945  34770  bnj1110  34979  f1resveqaeq  35082  cvmopnlem  35272  cvmfolem  35273  cvmliftmolem2  35276  cvmlift2lem10  35306  satf00  35368  satffunlem2lem1  35398  satefvfmla0  35412  mrsubvrs  35516  wzel  35819  btwnconn1lem8  36089  btwnconn1lem9  36090  btwnconn1lem10  36091  btwnconn1lem11  36092  btwnconn1lem12  36093  finminlem  36313  nn0prpwlem  36317  fnessref  36352  refssfne  36353  fnemeet2  36362  consym1  36415  bj-finsumval0  37280  topdifinffinlem  37342  relowlssretop  37358  rdgeqoa  37365  fvineqsneu  37406  pibt2  37412  matunitlindflem1  37617  poimirlem28  37649  mblfinlem1  37658  mblfinlem3  37660  mblfinlem4  37661  ovoliunnfl  37663  mbfresfi  37667  mbfposadd  37668  itg2addnclem2  37673  itg2addnc  37675  ftc1anc  37702  frinfm  37736  fdc  37746  blssp  37757  sstotbnd  37776  isbnd2  37784  ssbnd  37789  prdstotbnd  37795  prdsbnd2  37796  ismtyres  37809  heibor1lem  37810  rrnequiv  37836  rngoisocnv  37982  crngohomfo  38007  pridlc3  38074  membpartlem19  38810  prter3  38882  ax12eq  38941  ax12el  38942  cvratlem  39422  islvol2aN  39593  4atlem4b  39601  4atlem4c  39602  4atlem4d  39603  isline2  39775  isline3  39777  pclfinclN  39951  linepsubclN  39952  pexmidlem4N  39974  diaglbN  41056  dvhvaddcl  41096  dvhvaddcomN  41097  dvhvscacl  41104  djavalN  41136  dibglbN  41167  dihatexv  41339  djhval  41399  mapdrvallem2  41646  evlselvlem  42581  evlselv  42582  mhpind  42589  prjsprellsp  42606  elrfi  42689  nacsfix  42707  eldioph2  42757  lzenom  42765  rexrabdioph  42789  irrapxlem3  42819  pellexlem5  42828  pellex  42830  pell1234qrne0  42848  pell1234qrmulcl  42850  pell14qrdich  42864  pell1qrge1  42865  pellqrex  42874  rmxypairf1o  42907  rmxycomplete  42913  monotoddzzfi  42938  congadd  42962  jm2.19lem3  42987  jm2.19lem4  42988  jm2.25  42995  jm2.26a  42996  jm2.26lem3  42997  expdiophlem1  43017  wepwsolem  43038  lmhmfgsplit  43082  aaitgo  43158  mon1psubm  43195  deg1mhm  43196  succlg  43324  ofoacom  43357  iunrelexp0  43698  isotone2  44045  mnuprdlem4  44271  relpmin  44949  disjrnmpt2  45189  mullimc  45621  mullimcf  45628  climxrre  45755  fprodcncf  45905  stoweidlem17  46022  stoweidlem27  46032  stoweidlem54  46059  fourierdlem42  46154  fourierdlem62  46173  fourierdlem73  46184  fourierdlem76  46187  fourierdlem97  46208  sge0iunmptlemfi  46418  isomenndlem  46535  imarnf1pr  47287  smonoord  47376  fvelsetpreimafv  47392  iccpartiltu  47427  sprsymrelf1lem  47496  prproropf1olem3  47510  paireqne  47516  fmtnoprmfac1  47570  prmdvdsfmtnof1lem2  47590  gricushgr  47921  grimedg  47939  cycl3grtri  47950  gpgedg2iv  48062  pgnbgreunbgrlem2lem1  48108  pgnbgreunbgrlem2lem2  48109  rngcinvALTV  48268  funcringcsetcALTV2lem9  48290  ringcinvALTV  48302  funcringcsetclem9ALTV  48313  lmodvsmdi  48371  lincsum  48422  lindslinindimp2lem4  48454  nn0sumshdiglemB  48613  1arymaptf1  48635  2arymaptf1  48646  dmrnxp  48829  xpco2  48849  initopropd  49236  termopropd  49237  zeroopropd  49238  oduoppcciso  49559  lanpropd  49608  ranpropd  49609