Theorem ad2antll 726

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

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  simprr  770  simprrl  778  simprrr  779  simprr1  1220  simprr2  1221  simprr3  1222  prneimg  4800  fr2nr  5599  wereu2  5618  f1oprg  6813  fvtp1g  7130  funfvima3  7169  isof1oidb  7252  isomin  7265  weniso  7282  elovmpt3rab1  7592  sorpssi  7645  poseq  8046  suppofssd  8090  tfrlem9a  8288  oalimcl  8463  odi  8482  oeeui  8505  ralxpmap  8756  boxriin  8800  domdifsn  8920  domunsncan  8938  enfixsn  8947  disjen  9000  mapen  9007  mapxpen  9009  mapunen  9012  findcard2d  9032  unxpdomlem2  9117  unxpdomlem3  9118  findcard3OLD  9152  isfinite2  9167  marypha1lem  9291  marypha2  9297  supmo  9310  infmo  9353  card2inf  9413  brwdom2  9431  wemapwe  9555  rankonidlem  9686  rankxplim3  9739  djulf1o  9770  djurf1o  9771  infxpenlem  9871  infxpenc2lem1  9877  infxpenc2  9880  fseqenlem1  9882  fseqenlem2  9883  infpwfien  9920  dfac12lem2  10002  infunsdom1  10071  infunsdom  10072  infmap2  10076  fin2i2  10176  fin23lem28  10198  fin23lem32  10202  fin23lem34  10204  fin23lem40  10209  isf32lem2  10212  compssiso  10232  isfin1-3  10244  fin1a2lem10  10267  fin12  10271  hsmexlem4  10287  ac6num  10337  ttukeylem7  10373  axdclem2  10378  iundom2g  10398  fpwwe2lem11  10499  pwfseqlem3  10518  winalim2  10554  winafp  10555  wunex2  10596  grur1  10678  dedekindle  11241  00id  11252  receu  11722  lt2mul2div  11955  peano5uzi  12511  uzwo  12753  qbtwnre  13035  iooshf  13260  modmul1  13746  seqcl2  13843  seqfveq2  13847  seqid2  13871  seqdistr  13876  expcl2lem  13896  mulexpz  13925  expnlbnd2  14051  hashfun  14253  hashfacen  14267  hashfacenOLD  14268  hashf1lem1  14269  hashf1lem1OLD  14270  elss2prb  14302  fstwrdne0  14360  swrdsb0eq  14475  swrdswrd  14517  wrd2ind  14535  swrdccatin1  14537  pfxccatin12  14545  splid  14565  repswrevw  14599  cshwidxmod  14615  cshwidx0  14618  2cshw  14625  cshweqrep  14633  cshw1  14634  wwlktovfo  14773  relexpfld  14860  relexpindlem  14874  sqrlem6  15059  absexpz  15117  o1rlimmul  15428  iseralt  15496  summolem2  15528  fsumf1o  15535  fsum0diag2  15595  fsummulc2  15596  cvgcmpce  15630  incexclem  15648  prodmolem2  15745  fprodcl2lem  15760  fprodmul  15770  fprodrev  15787  moddvds  16074  dvdsflip  16126  bitsf1ocnv  16251  sadcaddlem  16264  bezoutlem2  16348  bezoutlem4  16350  dfgcd2  16354  lcmgcdlem  16409  crth  16577  hashgcdlem  16587  phisum  16589  pcqcl  16655  pcid  16672  pcneg  16673  prmpwdvds  16703  pockthg  16705  4sqlem11  16754  ramub2  16813  0ram  16819  prmgaplem7  16856  prmgaplem8  16857  setscom  16979  qusval  17351  initoeu1  17824  termoeu1  17831  setcinv  17903  funcestrcsetclem9  17963  funcsetcestrclem9  17978  fullsetcestrc  17981  1stfcl  18012  2ndfcl  18013  hofpropd  18083  isacs3lem  18358  frmdss2  18599  frmdup1  18600  mgm2nsgrplem2  18655  mulgdirlem  18831  mulgass  18837  0nsg  18894  cycsubgcl  18922  ghmmulg  18943  conjghm  18962  qusghm  18968  gsumwrev  19070  symg2bas  19097  symgfixelsi  19140  f1otrspeq  19152  psgnunilem2  19200  psgnunilem3  19201  odf1o2  19275  lsmhash  19407  efgtf  19424  efginvrel2  19429  efgredeu  19454  efgcpbllemb  19457  frgpuplem  19474  frgpup1  19477  cygablOLD  19588  ghmcyg  19593  gsumval3lem1  19602  gsumzres  19606  gsumzcl2  19607  gsumzf1o  19609  gsumzaddlem  19618  gsumconst  19631  gsumzmhm  19634  gsumzoppg  19641  gsum2d  19669  subgdmdprd  19733  pgpfac1lem3  19776  gsummgp0  19943  islmodd  20236  lmodvsmmulgdi  20265  islss3  20328  0lmhm  20409  idlmhm  20410  lmhmeql  20424  pwssplit3  20430  lidldvgen  20633  qsssubdrg  20764  cnsubrg  20765  znf1o  20866  psgnghm  20892  psgndif  20914  cssmre  21005  dsmmsubg  21057  frlmup1  21112  lindfrn  21135  f1lindf  21136  evlslem1  21399  coe1tmmul2  21554  pf1ind  21628  mamufval  21641  mamurid  21698  mvmulfval  21798  mdetralt2  21865  mndifsplit  21892  maducoeval2  21896  madugsum  21899  mat2pmatmul  21987  decpmatmul  22028  pm2mpf1lem  22050  pm2mpf1  22055  monmat2matmon  22080  chpscmat  22098  fvmptnn04if  22105  tgcl  22226  ppttop  22264  epttop  22266  clsval2  22308  opncldf1  22342  mretopd  22350  neindisj  22375  neiptopnei  22390  restcls  22439  restntr  22440  ordtbas  22450  cnpnei  22522  cncls2  22531  tgcmp  22659  cmpcld  22660  uncmp  22661  hauscmplem  22664  1stcfb  22703  2ndcctbss  22713  hauspwdom  22759  reftr  22772  comppfsc  22790  kgentopon  22796  ptpjpre1  22829  ptcnplem  22879  txcn  22884  txdis1cn  22893  txhaus  22905  xkopt  22913  imasnopn  22948  imasncld  22949  imasncls  22950  hmeoimaf1o  23028  cmphaushmeo  23058  txhmeo  23061  trfbas2  23101  fbasfip  23126  fbasrn  23142  fmss  23204  elfm2  23206  hauspwpwf1  23245  flfcnp  23262  fclscf  23283  flimfnfcls  23286  fcfval  23291  alexsubALTlem2  23306  alexsubALTlem3  23307  alexsubALTlem4  23308  ptcmplem3  23312  ptcmplem4  23313  cnextfval  23320  cnextcn  23325  tmdgsum2  23354  ustex2sym  23475  neipcfilu  23555  imasdsf1olem  23633  metss2lem  23774  stdbdxmet  23778  stdbdmopn  23781  metrest  23787  metcnp  23804  restmetu  23833  tngngp  23925  icccmplem1  24092  icccvx  24220  evth  24229  lebnumlem1  24231  pi1blem  24309  isncvsngp  24420  equivcau  24571  bcthlem5  24599  cmslssbn  24643  ivthlem3  24724  ovolicc2lem3  24790  ovolicc2lem4  24791  dyaddisj  24867  dyadmbllem  24870  ismbfd  24910  itg2seq  25014  itgss  25083  limciun  25165  dvcobr  25217  dvmptfsum  25246  c1liplem1  25267  c1lip1  25268  lhop  25287  dvcvx  25291  tdeglem4  25331  plyco0  25460  elply2  25464  plypf1  25480  dgreq0  25533  elqaalem2  25587  aalioulem6  25604  aaliou  25605  aaliou2b  25608  ulmss  25663  ulmcn  25665  pserulm  25688  lgamgulmlem5  26289  basellem4  26340  fsumdvdsdiaglem  26439  dvdsmulf1o  26450  chtublem  26466  fsumvma2  26469  logfaclbnd  26477  dchrelbasd  26494  lgsqrlem2  26602  gausslemma2dlem1a  26620  lgseisenlem2  26631  lgsquadlem1  26635  lgsquadlem2  26636  lgsquadlem3  26637  rplogsumlem2  26740  rpvmasumlem  26742  dchrmusum2  26749  dchrvmasumlem1  26750  dchrvmasum2lem  26751  rpvmasum2  26767  dchrisum0lem1  26771  logsqvma  26797  selberg4  26816  pntibndlem3  26847  pntlem3  26864  ostthlem1  26882  ostthlem2  26883  sltres  26917  nogt01o  26951  idmot  27188  brcgr  27558  brbtwn2  27563  axsegconlem8  27582  axpaschlem  27598  axeuclid  27621  axcontlem2  27623  axcontlem7  27628  eengtrkg  27644  upgrex  27752  subgrprop3  27933  subupgr  27944  nbgr0vtxlem  28012  nb3grprlem1  28037  cusgredg  28081  cusgrres  28105  usgredgsscusgredg  28116  finsumvtxdg2ssteplem4  28205  finsumvtxdg2sstep  28206  wlkl1loop  28295  wlkp1lem4  28333  wwlksnred  28546  wwlksnext  28547  wwlksnextwrd  28551  wpthswwlks2on  28615  clwwlknp  28690  clwwlkel  28699  wwlksext2clwwlk  28710  clwwlknonwwlknonb  28759  3wlkond  28824  1conngr  28847  eucrctshift  28896  fusgr2wsp2nb  28987  numclwwlk1lem2foa  29007  numclwwlk1lem2f1  29010  numclwlk1lem1  29022  numclwlk1lem2  29023  grpoidinvlem1  29155  grporcan  29169  ipblnfi  29506  hvmulcan2  29724  shscli  29968  spansneleq  30221  pjspansn  30228  3oalem2  30314  eigposi  30487  cnlnadjlem2  30719  stlesi  30892  mdslmd1lem1  30976  mdslmd1lem2  30977  cdj1i  31084  disjxpin  31214  nn0xmulclb  31381  xreceu  31483  txomap  32082  pstmxmet  32145  qqhghm  32236  qqhrhm  32237  measinblem  32486  cntmeas  32492  ballotlemsf1o  32780  bnj945  33052  bnj1110  33261  f1resveqaeq  33356  cvmopnlem  33539  cvmfolem  33540  cvmliftmolem2  33543  cvmlift2lem10  33573  satf00  33635  satffunlem2lem1  33665  satefvfmla0  33679  mrsubvrs  33783  poxp3  34080  wzel  34099  oldbdayim  34181  addsproplem2  34236  btwnconn1lem8  34535  btwnconn1lem9  34536  btwnconn1lem10  34537  btwnconn1lem11  34538  btwnconn1lem12  34539  finminlem  34646  nn0prpwlem  34650  fnessref  34685  refssfne  34686  fnemeet2  34695  consym1  34748  bj-finsumval0  35612  topdifinffinlem  35674  relowlssretop  35690  rdgeqoa  35697  fvineqsneu  35738  pibt2  35744  matunitlindflem1  35929  poimirlem28  35961  mblfinlem1  35970  mblfinlem3  35972  mblfinlem4  35973  ovoliunnfl  35975  mbfresfi  35979  mbfposadd  35980  itg2addnclem2  35985  itg2addnc  35987  ftc1anc  36014  frinfm  36049  fdc  36059  blssp  36070  sstotbnd  36089  isbnd2  36097  ssbnd  36102  prdstotbnd  36108  prdsbnd2  36109  ismtyres  36122  heibor1lem  36123  rrnequiv  36149  rngoisocnv  36295  crngohomfo  36320  pridlc3  36387  membpartlem19  37129  prter3  37200  ax12eq  37259  ax12el  37260  cvratlem  37740  islvol2aN  37911  4atlem4b  37919  4atlem4c  37920  4atlem4d  37921  isline2  38093  isline3  38095  pclfinclN  38269  linepsubclN  38270  pexmidlem4N  38292  diaglbN  39374  dvhvaddcl  39414  dvhvaddcomN  39415  dvhvscacl  39422  djavalN  39454  dibglbN  39485  dihatexv  39657  djhval  39717  mapdrvallem2  39964  metakunt15  40447  mhpind  40594  prjsprellsp  40761  elrfi  40829  nacsfix  40847  eldioph2  40897  lzenom  40905  rexrabdioph  40929  irrapxlem3  40959  pellexlem5  40968  pellex  40970  pell1234qrne0  40988  pell1234qrmulcl  40990  pell14qrdich  41004  pell1qrge1  41005  pellqrex  41014  rmxypairf1o  41047  rmxycomplete  41053  monotoddzzfi  41078  congadd  41102  jm2.19lem3  41127  jm2.19lem4  41128  jm2.25  41135  jm2.26a  41136  jm2.26lem3  41137  expdiophlem1  41157  wepwsolem  41181  lmhmfgsplit  41225  aaitgo  41301  mon1psubm  41345  deg1mhm  41346  succlg  41366  ofoacom  41379  iunrelexp0  41683  isotone2  42032  mnuprdlem4  42266  disjrnmpt2  43105  mullimc  43545  mullimcf  43552  climxrre  43679  fprodcncf  43829  stoweidlem17  43946  stoweidlem27  43956  stoweidlem54  43983  fourierdlem42  44078  fourierdlem62  44097  fourierdlem73  44108  fourierdlem76  44111  fourierdlem97  44132  sge0iunmptlemfi  44340  isomenndlem  44457  imarnf1pr  45192  smonoord  45241  fvelsetpreimafv  45257  iccpartiltu  45292  sprsymrelf1lem  45361  prproropf1olem3  45375  paireqne  45381  fmtnoprmfac1  45435  prmdvdsfmtnof1lem2  45455  isomushgr  45696  isomuspgrlem2c  45700  mgmhmlin  45758  rnghmmul  45876  rngcinv  45957  rngcinvALTV  45969  ringcinv  46008  funcringcsetcALTV2lem9  46020  ringcinvALTV  46032  funcringcsetclem9ALTV  46043  mndpsuppss  46125  lmodvsmdi  46136  lincsum  46188  lindslinindimp2lem4  46220  nn0sumshdiglemB  46384  1arymaptf1  46406  2arymaptf1  46417