Theorem ad2antll 742

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprr  785  simprrl  793  simprrr  794  simprr1  1240  simprr2  1241  simprr3  1242  prneimg  4812  prproe  4836  fr2nr  5632  wereu2  5652  f1oprg  6882  fvtp1g  7213  funfvima3  7252  f1resveqaeq  7287  isof1oidb  7342  isomin  7355  weniso  7374  elovmpt3rab1  7691  sorpssi  7755  resf1extb  7956  poseq  8188  suppofssd  8234  tfrlem9a  8408  oalimcl  8582  odi  8601  oeeui  8625  ralxpmap  8938  boxriin  8982  domdifsn  9093  domunsncan  9110  enfixsn  9119  disjen  9167  mapen  9174  mapxpen  9176  mapunen  9179  findcard2d  9196  unxpdomlem2  9262  unxpdomlem3  9263  isfinite2  9304  marypha1lem  9438  marypha2  9444  supmo  9457  infmo  9502  card2inf  9562  brwdom2  9580  wemapwe  9711  rankonidlem  9851  rankxplim3  9911  rankfilimbi  9915  djulf1o  10006  djurf1o  10007  infxpenlem  10105  infxpenc2lem1  10111  infxpenc2  10114  fseqenlem1  10116  fseqenlem2  10117  infpwfien  10154  dfac12lem2  10236  infunsdom1  10303  infunsdom  10304  infmap2  10308  fin2i2  10409  fin23lem28  10431  fin23lem32  10435  fin23lem34  10437  fin23lem40  10442  isf32lem2  10445  compssiso  10465  isfin1-3  10477  fin1a2lem10  10500  fin12  10504  hsmexlem4  10520  ac6num  10570  ttukeylem7  10606  axdclem2  10611  iundom2g  10637  fpwwe2lem11  10739  pwfseqlem3  10758  winalim2  10794  winafp  10795  wunex2  10836  grur1  10918  dedekindle  11487  00id  11498  receu  11974  lt2mul2div  12208  peano5uzi  12801  uzwo  13051  qbtwnre  13342  iooshf  13570  modmul1  14080  seqcl2  14176  seqfveq2  14180  seqid2  14204  seqdistr  14209  expcl2lem  14229  mulexpz  14258  expnlbnd2  14391  hashfun  14595  hashfacen  14612  hashf1lem1  14613  elss2prb  14646  fstwrdne0  14714  swrdsb0eq  14827  swrdswrd  14868  wrd2ind  14886  swrdccatin1  14888  pfxccatin12  14896  splid  14916  repswrevw  14952  cshwidxmod  14968  cshwidx0  14971  2cshw  14978  cshweqrep  14986  cshw1  14987  wwlktovfo  15126  relexpfld  15217  relexpindlem  15231  01sqrexlem6  15429  absexpz  15487  o1rlimmul  15801  iseralt  15867  summolem2  15897  fsumf1o  15904  fsum0diag2  15964  fsummulc2  15965  cvgcmpce  16000  incexclem  16020  prodmolem2  16117  fprodcl2lem  16132  fprodmul  16142  fprodrev  16159  moddvds  16448  dvdsflip  16502  bitsf1ocnv  16629  sadcaddlem  16642  bezoutlem2  16728  bezoutlem4  16730  dfgcd2  16734  lcmgcdlem  16796  crth  16970  hashgcdlem  16980  phisum  16983  pcqcl  17049  pcid  17066  pcneg  17067  prmpwdvds  17097  pockthg  17099  4sqlem11  17148  ramub2  17207  0ram  17213  prmgaplem7  17250  prmgaplem8  17251  setscom  17373  qusval  17729  initoeu1  18201  termoeu1  18208  setcinv  18280  funcestrcsetclem9  18337  funcsetcestrclem9  18352  fullsetcestrc  18355  1stfcl  18386  2ndfcl  18387  hofpropd  18456  isacs3lem  18731  mgmhmlin  18903  mndpsuppss  18974  frmdss2  19074  frmdup1  19075  mgm2nsgrplem2  19133  mulgdirlem  19330  mulgass  19336  0nsg  19394  cycsubgcl  19436  ghmmulg  19457  conjghm  19478  qusghm  19484  gsumwrev  19595  symg2bas  19622  symgfixelsi  19664  f1otrspeq  19676  psgnunilem2  19724  psgnunilem3  19725  odf1o2  19802  lsmhash  19934  efgtf  19951  efginvrel2  19956  efgredeu  19981  efgcpbllemb  19984  frgpuplem  20001  frgpup1  20004  ghmcyg  20125  gsumval3lem1  20134  gsumzres  20138  gsumzcl2  20139  gsumzf1o  20141  gsumzaddlem  20150  gsumconst  20163  gsumzmhm  20166  gsumzoppg  20173  gsum2d  20201  subgdmdprd  20265  pgpfac1lem3  20308  gsummgp0  20562  rnghmmul  20694  rngcinv  20904  ringcinv  20938  islmodd  21156  lmodvsmmulgdi  21187  islss3  21249  0lmhm  21330  idlmhm  21331  lmhmeql  21345  pwssplit3  21351  cmprmidlmcl  21646  lidldvgen  21673  qsssubdrg  21747  cnsubrg  21748  znf1o  21872  psgnghm  21901  psgndif  21923  cssmre  22014  dsmmsubg  22064  frlmup1  22119  lindfrn  22142  f1lindf  22143  evlslem1  22406  psdmul  22502  coe1tmmul2  22610  pf1ind  22688  mamufval  22722  mamurid  22772  mvmulfval  22872  mdetralt2  22939  mndifsplit  22966  maducoeval2  22970  madugsum  22973  matunitlindflem1  23009  mat2pmatmul  23064  decpmatmul  23105  pm2mpf1lem  23127  pm2mpf1  23132  monmat2matmon  23157  chpscmat  23175  fvmptnn04if  23182  tgcl  23302  ppttop  23340  epttop  23342  clsval2  23383  opncldf1  23417  mretopd  23425  neindisj  23450  neiptopnei  23465  restcls  23514  restntr  23515  ordtbas  23525  cnpnei  23597  cncls2  23606  tgcmp  23734  cmpcld  23735  uncmp  23736  hauscmplem  23739  1stcfb  23778  2ndcctbss  23789  hauspwdom  23835  reftr  23848  comppfsc  23866  kgentopon  23872  ptpjpre1  23905  ptcnplem  23955  txcn  23960  txdis1cn  23969  txhaus  23981  xkopt  23989  imasnopn  24024  imasncld  24025  imasncls  24026  hmeoimaf1o  24104  cmphaushmeo  24134  txhmeo  24137  trfbas2  24177  fbasfip  24202  fbasrn  24218  fmss  24280  elfm2  24282  hauspwpwf1  24321  flfcnp  24338  fclscf  24359  flimfnfcls  24362  fcfval  24367  alexsubALTlem2  24382  alexsubALTlem3  24383  alexsubALTlem4  24384  ptcmplem3  24388  ptcmplem4  24389  cnextfval  24396  cnextcn  24401  tmdgsum2  24430  ustex2sym  24551  neipcfilu  24629  imasdsf1olem  24707  metss2lem  24845  stdbdxmet  24849  stdbdmopn  24852  metrest  24858  metcnp  24875  restmetu  24904  tngngp  24988  icccmplem1  25157  icccvx  25286  evth  25295  lebnumlem1  25297  pi1blem  25375  isncvsngp  25485  equivcau  25636  bcthlem5  25664  cmslssbn  25708  ivthlem3  25789  ovolicc2lem3  25855  ovolicc2lem4  25856  dyaddisj  25932  dyadmbllem  25935  ismbfd  25975  itg2seq  26078  itgss  26147  limciun  26229  dvcobr  26281  dvmptfsum  26310  c1liplem1  26331  c1lip1  26332  lhop  26351  dvcvx  26355  tdeglem4  26393  plyco0  26525  elply2  26529  plypf1  26546  dgreq0  26599  elqaalem2  26658  aalioulem6  26679  aaliou  26680  aaliou2b  26683  ulmss  26739  ulmcn  26741  pserulm  26764  lgamgulmlem5  27375  basellem4  27426  fsumdvdsdiaglem  27525  mpodvdsmulf1o  27536  dvdsmulf1o  27538  chtublem  27553  fsumvma2  27556  logfaclbnd  27564  dchrelbasd  27581  lgsqrlem2  27689  gausslemma2dlem1a  27707  lgseisenlem2  27718  lgsquadlem1  27722  lgsquadlem2  27723  lgsquadlem3  27724  rplogsumlem2  27827  rpvmasumlem  27829  dchrmusum2  27836  dchrvmasumlem1  27837  dchrvmasum2lem  27838  rpvmasum2  27854  dchrisum0lem1  27858  logsqvma  27884  selberg4  27903  pntibndlem3  27934  pntlem3  27951  ostthlem1  27969  ostthlem2  27970  ltsres  28034  nogt01o  28068  oldbdayim  28290  addsproplem2  28371  negsproplem2  28430  mulsval  28510  om2noseqrdg  28705  noseqrdgfn  28707  zmulscld  28798  recut  28895  idmot  29015  brcgr  29493  brbtwn2  29498  axsegconlem8  29517  axpaschlem  29533  axeuclid  29556  axcontlem2  29558  axcontlem7  29563  eengtrkg  29579  upgrex  29685  subgrprop3  29872  subupgr  29883  nbgr0edglem  29952  nb3grprlem1  29976  cusgredg  30020  cusgrres  30044  usgredgsscusgredg  30055  finsumvtxdg2ssteplem4  30144  finsumvtxdg2sstep  30145  wlkl1loop  30233  wlkp1lem4  30270  wwlksnred  30496  wwlksnext  30497  wwlksnextwrd  30501  wpthswwlks2on  30568  clwwlknp  30643  clwwlkel  30652  wwlksext2clwwlk  30663  clwwlknonwwlknonb  30712  3wlkond  30787  1conngr  30810  eucrctshift  30859  fusgr2wsp2nb  30950  numclwwlk1lem2foa  30970  numclwwlk1lem2f1  30973  numclwlk1lem1  30985  numclwlk1lem2  30986  grpoidinvlem1  31121  grporcan  31135  ipblnfi  31472  hvmulcan2  31690  shscli  31934  spansneleq  32187  pjspansn  32194  3oalem2  32280  eigposi  32453  cnlnadjlem2  32685  stlesi  32858  mdslmd1lem1  32942  mdslmd1lem2  32943  cdj1i  33050  disjxpin  33239  nn0xmulclb  33419  xreceu  33544  txomap  34522  pstmxmet  34585  qqhghm  34676  qqhrhm  34677  measinblem  34909  cntmeas  34915  ballotlemsf1o  35202  bnj945  35460  bnj1110  35668  cvmopnlem  36167  cvmfolem  36168  cvmliftmolem2  36171  cvmlift2lem10  36201  satf00  36263  satffunlem2lem1  36293  satefvfmla0  36307  mrsubvrs  36411  wzel  36716  btwnconn1lem8  36989  btwnconn1lem9  36990  btwnconn1lem10  36991  btwnconn1lem11  36992  btwnconn1lem12  36993  finminlem  37236  nn0prpwlem  37240  fnessref  37275  refssfne  37276  fnemeet2  37285  consym1  37338  bj-finsumval0  38349  topdifinffinlem  38413  relowlssretop  38429  rdgeqoa  38436  fvineqsneu  38477  pibt2  38483  poimirlem28  38709  mblfinlem1  38718  mblfinlem3  38720  mblfinlem4  38721  ovoliunnfl  38723  mbfresfi  38727  mbfposadd  38728  itg2addnclem2  38733  itg2addnc  38735  ftc1anc  38762  frinfm  38812  fdc  38822  blssp  38833  sstotbnd  38852  isbnd2  38860  ssbnd  38865  prdstotbnd  38871  prdsbnd2  38872  ismtyres  38885  heibor1lem  38886  rrnequiv  38912  rngoisocnv  39058  crngohomfo  39083  pridlc3  39150  membpartlem19  39989  prter3  40082  ax12eq  40141  ax12el  40142  cvratlem  40621  islvol2aN  40792  4atlem4b  40800  4atlem4c  40801  4atlem4d  40802  isline2  40974  isline3  40976  pclfinclN  41150  linepsubclN  41151  pexmidlem4N  41173  diaglbN  42255  dvhvaddcl  42295  dvhvaddcomN  42296  dvhvscacl  42303  djavalN  42335  dibglbN  42366  dihatexv  42538  djhval  42598  mapdrvallem2  42845  evlselvlem  43759  evlselv  43760  mhpind  43765  prjsprellsp  43782  elrfi  43848  nacsfix  43866  eldioph2  43916  lzenom  43924  rexrabdioph  43944  irrapxlem3  43974  pellexlem5  43983  pellex  43985  pell1234qrne0  44003  pell1234qrmulcl  44005  pell14qrdich  44019  pell1qrge1  44020  pellqrex  44029  rmxypairf1o  44061  rmxycomplete  44067  monotoddzzfi  44092  congadd  44116  jm2.19lem3  44141  jm2.19lem4  44142  jm2.25  44149  jm2.26a  44150  jm2.26lem3  44151  expdiophlem1  44171  wepwsolem  44192  lmhmfgsplit  44231  aaitgo  44307  mon1psubm  44344  deg1mhm  44345  succlg  44473  ofoacom  44506  iunrelexp0  44845  isotone2  45192  mnuprdlem4  45402  relpmin  46084  disjrnmpt2  46345  mullimc  46770  mullimcf  46777  climxrre  46902  fprodcncf  47052  stoweidlem17  47169  stoweidlem27  47179  stoweidlem54  47206  fourierdlem42  47301  fourierdlem62  47320  fourierdlem73  47331  fourierdlem76  47334  fourierdlem97  47355  sge0iunmptlemfi  47565  isomenndlem  47682  imarnf1pr  48494  smonoord  48589  fvelsetpreimafv  48611  iccpartiltu  48646  sprsymrelf1lem  48715  prproropf1olem3  48729  paireqne  48735  fmtnoprmfac1  48792  prmdvdsfmtnof1lem2  48812  nprmdvdsfacm1  48851  gricushgr  49157  grimedg  49175  cycl3grtri  49187  gpgedg2iv  49307  pgnbgreunbgrlem2lem1  49354  pgnbgreunbgrlem2lem2  49355  rngcinvALTV  49515  funcringcsetcALTV2lem9  49537  ringcinvALTV  49549  funcringcsetclem9ALTV  49560  lmodvsmdi  49633  lincsum  49683  lindslinindimp2lem4  49715  nn0sumshdiglemB  49874  1arymaptf1  49896  2arymaptf1  49907  dmrnxp  50090  xpco2  50110  initopropd  50507  termopropd  50508  zeroopropd  50509  oduoppcciso  50846  lanpropd  50940  ranpropd  50941