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  4788  fr2nr  5536  wereu2  5555  f1oprg  6662  fvtp1g  6963  funfvima3  7001  isof1oidb  7080  isomin  7093  weniso  7110  elovmpt3rab1  7408  sorpssi  7458  suppofssd  7870  tfrlem9a  8025  oalimcl  8189  odi  8208  oeeui  8231  ralxpmap  8463  boxriin  8507  domdifsn  8603  domunsncan  8620  enfixsn  8629  disjen  8677  mapen  8684  mapxpen  8686  mapunen  8689  unxpdomlem2  8726  unxpdomlem3  8727  findcard2d  8763  findcard3  8764  isfinite2  8779  marypha1lem  8900  marypha2  8906  supmo  8919  infmo  8962  card2inf  9022  brwdom2  9040  wemapwe  9163  rankonidlem  9260  rankxplim3  9313  djulf1o  9344  djurf1o  9345  infxpenlem  9442  infxpenc2lem1  9448  infxpenc2  9451  fseqenlem1  9453  fseqenlem2  9454  infpwfien  9491  dfac12lem2  9573  infunsdom1  9638  infunsdom  9639  infmap2  9643  fin2i2  9743  fin23lem28  9765  fin23lem32  9769  fin23lem34  9771  fin23lem40  9776  isf32lem2  9779  compssiso  9799  isfin1-3  9811  fin1a2lem10  9834  fin12  9838  hsmexlem4  9854  ac6num  9904  ttukeylem7  9940  axdclem2  9945  iundom2g  9965  fpwwe2lem12  10066  pwfseqlem3  10085  winalim2  10121  winafp  10122  wunex2  10163  grur1  10245  dedekindle  10807  00id  10818  receu  11288  lt2mul2div  11521  peano5uzi  12074  uzwo  12314  qbtwnre  12595  iooshf  12818  modmul1  13295  seqcl2  13391  seqfveq2  13395  seqid2  13419  seqdistr  13424  expcl2lem  13444  mulexpz  13472  expnlbnd2  13598  hashfun  13801  hashfacen  13815  hashf1lem1  13816  elss2prb  13848  fstwrdne0  13911  swrdsb0eq  14028  swrdswrd  14070  wrd2ind  14088  swrdccatin1  14090  pfxccatin12  14098  splid  14118  repswrevw  14152  cshwidxmod  14168  cshwidx0  14171  2cshw  14178  cshweqrep  14186  cshw1  14187  wwlktovfo  14325  relexpfld  14411  relexpindlem  14425  sqrlem6  14610  absexpz  14668  o1rlimmul  14978  iseralt  15044  summolem2  15076  fsumf1o  15083  fsum0diag2  15141  fsummulc2  15142  cvgcmpce  15176  incexclem  15194  prodmolem2  15292  fprodcl2lem  15307  fprodmul  15317  fprodrev  15334  moddvds  15621  dvdsflip  15670  bitsf1ocnv  15796  sadcaddlem  15809  bezoutlem2  15891  bezoutlem4  15893  dfgcd2  15897  lcmgcdlem  15953  crth  16118  hashgcdlem  16128  phisum  16130  pcqcl  16196  pcid  16212  pcneg  16213  prmpwdvds  16243  pockthg  16245  4sqlem11  16294  ramub2  16353  0ram  16359  prmgaplem7  16396  prmgaplem8  16397  setscom  16530  qusval  16818  initoeu1  17274  termoeu1  17281  setcinv  17353  funcestrcsetclem9  17401  funcsetcestrclem9  17416  fullsetcestrc  17419  1stfcl  17450  2ndfcl  17451  hofpropd  17520  isacs3lem  17779  frmdss2  18031  frmdup1  18032  mgm2nsgrplem2  18087  mulgdirlem  18261  mulgass  18267  0nsg  18324  cycsubgcl  18352  ghmmulg  18373  conjghm  18392  qusghm  18398  gsumwrev  18497  symg2bas  18524  symgfixelsi  18566  f1otrspeq  18578  psgnunilem2  18626  psgnunilem3  18627  odf1o2  18701  lsmhash  18834  efgtf  18851  efginvrel2  18856  efgredeu  18881  efgcpbllemb  18884  frgpuplem  18901  frgpup1  18904  cygablOLD  19014  ghmcyg  19019  gsumval3lem1  19028  gsumzres  19032  gsumzcl2  19033  gsumzf1o  19035  gsumzaddlem  19044  gsumconst  19057  gsumzmhm  19060  gsumzoppg  19067  gsum2d  19095  subgdmdprd  19159  pgpfac1lem3  19202  gsummgp0  19361  islmodd  19643  lmodvsmmulgdi  19672  islss3  19734  0lmhm  19815  idlmhm  19816  lmhmeql  19830  pwssplit3  19836  lidldvgen  20031  evlslem1  20298  coe1tmmul2  20447  pf1ind  20521  qsssubdrg  20607  cnsubrg  20608  znf1o  20701  psgnghm  20727  psgndif  20749  cssmre  20840  dsmmsubg  20890  frlmup1  20945  lindfrn  20968  f1lindf  20969  mamufval  20999  mamurid  21054  mvmulfval  21154  mdetralt2  21221  mndifsplit  21248  maducoeval2  21252  madugsum  21255  mat2pmatmul  21342  decpmatmul  21383  pm2mpf1lem  21405  pm2mpf1  21410  monmat2matmon  21435  chpscmat  21453  fvmptnn04if  21460  tgcl  21580  ppttop  21618  epttop  21620  clsval2  21661  opncldf1  21695  mretopd  21703  neindisj  21728  neiptopnei  21743  restcls  21792  restntr  21793  ordtbas  21803  cnpnei  21875  cncls2  21884  tgcmp  22012  cmpcld  22013  uncmp  22014  hauscmplem  22017  1stcfb  22056  2ndcctbss  22066  hauspwdom  22112  reftr  22125  comppfsc  22143  kgentopon  22149  ptpjpre1  22182  ptcnplem  22232  txcn  22237  txdis1cn  22246  txhaus  22258  xkopt  22266  imasnopn  22301  imasncld  22302  imasncls  22303  hmeoimaf1o  22381  cmphaushmeo  22411  txhmeo  22414  trfbas2  22454  fbasfip  22479  fbasrn  22495  fmss  22557  elfm2  22559  hauspwpwf1  22598  flfcnp  22615  fclscf  22636  flimfnfcls  22639  fcfval  22644  alexsubALTlem2  22659  alexsubALTlem3  22660  alexsubALTlem4  22661  ptcmplem3  22665  ptcmplem4  22666  cnextfval  22673  cnextcn  22678  tmdgsum2  22707  ustex2sym  22828  neipcfilu  22908  imasdsf1olem  22986  metss2lem  23124  stdbdxmet  23128  stdbdmopn  23131  metrest  23137  metcnp  23154  restmetu  23183  tngngp  23266  icccmplem1  23433  icccvx  23557  evth  23566  lebnumlem1  23568  pi1blem  23646  isncvsngp  23756  equivcau  23906  bcthlem5  23934  cmslssbn  23978  ivthlem3  24057  ovolicc2lem3  24123  ovolicc2lem4  24124  dyaddisj  24200  dyadmbllem  24203  ismbfd  24243  itg2seq  24346  itgss  24415  limciun  24495  dvcobr  24546  dvmptfsum  24575  c1liplem1  24596  c1lip1  24597  lhop  24616  dvcvx  24620  plyco0  24785  elply2  24789  plypf1  24805  dgreq0  24858  elqaalem2  24912  aalioulem6  24929  aaliou  24930  aaliou2b  24933  ulmss  24988  ulmcn  24990  pserulm  25013  lgamgulmlem5  25613  basellem4  25664  fsumdvdsdiaglem  25763  dvdsmulf1o  25774  chtublem  25790  fsumvma2  25793  logfaclbnd  25801  dchrelbasd  25818  lgsqrlem2  25926  gausslemma2dlem1a  25944  lgseisenlem2  25955  lgsquadlem1  25959  lgsquadlem2  25960  lgsquadlem3  25961  rplogsumlem2  26064  rpvmasumlem  26066  dchrmusum2  26073  dchrvmasumlem1  26074  dchrvmasum2lem  26075  rpvmasum2  26091  dchrisum0lem1  26095  logsqvma  26121  selberg4  26140  pntibndlem3  26171  pntlem3  26188  ostthlem1  26206  ostthlem2  26207  idmot  26326  brcgr  26689  brbtwn2  26694  axsegconlem8  26713  axpaschlem  26729  axeuclid  26752  axcontlem2  26754  axcontlem7  26759  eengtrkg  26775  upgrex  26880  subgrprop3  27061  subupgr  27072  nbgr0vtxlem  27140  nb3grprlem1  27165  cusgredg  27209  cusgrres  27233  usgredgsscusgredg  27244  finsumvtxdg2ssteplem4  27333  finsumvtxdg2sstep  27334  wlkl1loop  27422  wlkp1lem4  27461  wwlksnred  27673  wwlksnext  27674  wwlksnextwrd  27678  wpthswwlks2on  27743  clwwlknp  27818  clwwlkel  27828  wwlksext2clwwlk  27839  clwwlknonwwlknonb  27888  3wlkond  27953  1conngr  27976  eucrctshift  28025  fusgr2wsp2nb  28116  numclwwlk1lem2foa  28136  numclwwlk1lem2f1  28139  numclwlk1lem1  28151  numclwlk1lem2  28152  grpoidinvlem1  28284  grporcan  28298  ipblnfi  28635  hvmulcan2  28853  shscli  29097  spansneleq  29350  pjspansn  29357  3oalem2  29443  eigposi  29616  cnlnadjlem2  29848  stlesi  30021  mdslmd1lem1  30105  mdslmd1lem2  30106  cdj1i  30213  disjxpin  30341  nn0xmulclb  30499  xreceu  30602  txomap  31102  pstmxmet  31141  qqhghm  31233  qqhrhm  31234  measinblem  31483  cntmeas  31489  ballotlemsf1o  31775  bnj945  32049  bnj1110  32258  f1resveqaeq  32362  cvmopnlem  32529  cvmfolem  32530  cvmliftmolem2  32533  cvmlift2lem10  32563  satf00  32625  satffunlem2lem1  32655  satefvfmla0  32669  mrsubvrs  32773  poseq  33099  wzel  33115  sltres  33173  sslttr  33272  btwnconn1lem8  33559  btwnconn1lem9  33560  btwnconn1lem10  33561  btwnconn1lem11  33562  btwnconn1lem12  33563  finminlem  33670  nn0prpwlem  33674  fnessref  33709  refssfne  33710  fnemeet2  33719  consym1  33772  bj-finsumval0  34571  topdifinffinlem  34632  relowlssretop  34648  rdgeqoa  34655  fvineqsneu  34696  pibt2  34702  matunitlindflem1  34892  poimirlem28  34924  mblfinlem1  34933  mblfinlem3  34935  mblfinlem4  34936  ovoliunnfl  34938  mbfresfi  34942  mbfposadd  34943  itg2addnclem2  34948  itg2addnc  34950  ftc1anc  34979  frinfm  35014  fdc  35024  blssp  35035  sstotbnd  35057  isbnd2  35065  ssbnd  35070  prdstotbnd  35076  prdsbnd2  35077  ismtyres  35090  heibor1lem  35091  rrnequiv  35117  rngoisocnv  35263  crngohomfo  35288  pridlc3  35355  prter3  36022  ax12eq  36081  ax12el  36082  cvratlem  36561  islvol2aN  36732  4atlem4b  36740  4atlem4c  36741  4atlem4d  36742  isline2  36914  isline3  36916  pclfinclN  37090  linepsubclN  37091  pexmidlem4N  37113  diaglbN  38195  dvhvaddcl  38235  dvhvaddcomN  38236  dvhvscacl  38243  djavalN  38275  dibglbN  38306  dihatexv  38478  djhval  38538  mapdrvallem2  38785  prjsprellsp  39267  elrfi  39297  nacsfix  39315  eldioph2  39365  lzenom  39373  rexrabdioph  39397  irrapxlem3  39427  pellexlem5  39436  pellex  39438  pell1234qrne0  39456  pell1234qrmulcl  39458  pell14qrdich  39472  pell1qrge1  39473  pellqrex  39482  rmxypairf1o  39514  rmxycomplete  39520  monotoddzzfi  39545  congadd  39569  jm2.19lem3  39594  jm2.19lem4  39595  jm2.25  39602  jm2.26a  39603  jm2.26lem3  39604  expdiophlem1  39624  wepwsolem  39648  lmhmfgsplit  39692  aaitgo  39768  mon1psubm  39812  deg1mhm  39813  iunrelexp0  40053  isotone2  40405  mnuprdlem4  40617  disjrnmpt2  41455  mullimc  41903  mullimcf  41910  climxrre  42037  fprodcncf  42190  stoweidlem17  42309  stoweidlem27  42319  stoweidlem54  42346  fourierdlem42  42441  fourierdlem62  42460  fourierdlem73  42471  fourierdlem76  42474  fourierdlem97  42495  sge0iunmptlemfi  42702  isomenndlem  42819  ovnsslelem  42849  imarnf1pr  43488  smonoord  43538  fvelsetpreimafv  43554  iccpartiltu  43589  sprsymrelf1lem  43660  prproropf1olem3  43674  paireqne  43680  fmtnoprmfac1  43734  prmdvdsfmtnof1lem2  43754  isomushgr  43998  isomuspgrlem2c  44002  mgmhmlin  44060  rnghmmul  44178  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  funcringcsetcALTV2lem9  44322  ringcinvALTV  44334  funcringcsetclem9ALTV  44345  mndpsuppss  44426  lmodvsmdi  44437  lincsum  44491  lindslinindimp2lem4  44523  nn0sumshdiglemB  44687