Theorem ad2antll 741

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  simprr  784  simprrl  792  simprrr  793  simprr1  1240  simprr2  1241  simprr3  1242  prneimg  4819  prproe  4870  fr2nr  5638  wereu2  5658  f1oprg  6867  fvtp1g  7196  funfvima3  7234  isof1oidb  7322  isomin  7335  weniso  7352  elovmpt3rab1  7670  sorpssi  7726  resf1extb  7927  poseq  8150  suppofssd  8195  tfrlem9a  8369  oalimcl  8541  odi  8560  oeeui  8584  ralxpmap  8890  boxriin  8934  domdifsn  9044  domunsncan  9061  enfixsn  9070  disjen  9118  mapen  9125  mapxpen  9127  mapunen  9130  findcard2d  9147  unxpdomlem2  9213  unxpdomlem3  9214  isfinite2  9254  marypha1lem  9389  marypha2  9395  supmo  9408  infmo  9453  card2inf  9513  brwdom2  9531  wemapwe  9662  rankonidlem  9796  rankxplim3  9849  djulf1o  9894  djurf1o  9895  infxpenlem  9993  infxpenc2lem1  9999  infxpenc2  10002  fseqenlem1  10004  fseqenlem2  10005  infpwfien  10042  dfac12lem2  10124  infunsdom1  10191  infunsdom  10192  infmap2  10196  fin2i2  10297  fin23lem28  10319  fin23lem32  10323  fin23lem34  10325  fin23lem40  10330  isf32lem2  10333  compssiso  10353  isfin1-3  10365  fin1a2lem10  10388  fin12  10392  hsmexlem4  10408  ac6num  10458  ttukeylem7  10494  axdclem2  10499  iundom2g  10519  fpwwe2lem11  10621  pwfseqlem3  10640  winalim2  10676  winafp  10677  wunex2  10718  grur1  10800  dedekindle  11369  00id  11380  receu  11854  lt2mul2div  12088  peano5uzi  12680  uzwo  12930  qbtwnre  13220  iooshf  13448  modmul1  13956  seqcl2  14052  seqfveq2  14056  seqid2  14080  seqdistr  14085  expcl2lem  14105  mulexpz  14134  expnlbnd2  14266  hashfun  14470  hashfacen  14487  hashf1lem1  14488  elss2prb  14521  fstwrdne0  14589  swrdsb0eq  14697  swrdswrd  14738  wrd2ind  14756  swrdccatin1  14758  pfxccatin12  14766  splid  14786  repswrevw  14820  cshwidxmod  14836  cshwidx0  14839  2cshw  14846  cshweqrep  14854  cshw1  14855  wwlktovfo  14991  relexpfld  15082  relexpindlem  15096  01sqrexlem6  15294  absexpz  15352  o1rlimmul  15666  iseralt  15732  summolem2  15763  fsumf1o  15770  fsum0diag2  15830  fsummulc2  15831  cvgcmpce  15866  incexclem  15886  prodmolem2  15985  fprodcl2lem  16000  fprodmul  16010  fprodrev  16027  moddvds  16316  dvdsflip  16370  bitsf1ocnv  16497  sadcaddlem  16510  bezoutlem2  16593  bezoutlem4  16595  dfgcd2  16599  lcmgcdlem  16659  crth  16832  hashgcdlem  16842  phisum  16845  pcqcl  16911  pcid  16928  pcneg  16929  prmpwdvds  16959  pockthg  16961  4sqlem11  17010  ramub2  17069  0ram  17075  prmgaplem7  17112  prmgaplem8  17113  setscom  17235  qusval  17591  initoeu1  18063  termoeu1  18070  setcinv  18142  funcestrcsetclem9  18199  funcsetcestrclem9  18214  fullsetcestrc  18217  1stfcl  18248  2ndfcl  18249  hofpropd  18318  isacs3lem  18593  mgmhmlin  18752  mndpsuppss  18818  frmdss2  18917  frmdup1  18918  mgm2nsgrplem2  18976  mulgdirlem  19166  mulgass  19172  0nsg  19230  cycsubgcl  19272  ghmmulg  19293  conjghm  19314  qusghm  19320  gsumwrev  19431  symg2bas  19458  symgfixelsi  19500  f1otrspeq  19512  psgnunilem2  19560  psgnunilem3  19561  odf1o2  19638  lsmhash  19770  efgtf  19787  efginvrel2  19792  efgredeu  19817  efgcpbllemb  19820  frgpuplem  19837  frgpup1  19840  ghmcyg  19961  gsumval3lem1  19970  gsumzres  19974  gsumzcl2  19975  gsumzf1o  19977  gsumzaddlem  19986  gsumconst  19999  gsumzmhm  20002  gsumzoppg  20009  gsum2d  20037  subgdmdprd  20101  pgpfac1lem3  20144  gsummgp0  20395  rnghmmul  20527  rngcinv  20736  ringcinv  20770  islmodd  20987  lmodvsmmulgdi  21018  islss3  21080  0lmhm  21161  idlmhm  21162  lmhmeql  21176  pwssplit3  21182  cmprmidlmcl  21475  lidldvgen  21502  qsssubdrg  21576  cnsubrg  21577  znf1o  21701  psgnghm  21730  psgndif  21752  cssmre  21843  dsmmsubg  21893  frlmup1  21948  lindfrn  21971  f1lindf  21972  evlslem1  22233  psdmul  22329  coe1tmmul2  22437  pf1ind  22515  mamufval  22549  mamurid  22599  mvmulfval  22699  mdetralt2  22766  mndifsplit  22793  maducoeval2  22797  madugsum  22800  mat2pmatmul  22888  decpmatmul  22929  pm2mpf1lem  22951  pm2mpf1  22956  monmat2matmon  22981  chpscmat  22999  fvmptnn04if  23006  tgcl  23126  ppttop  23164  epttop  23166  clsval2  23207  opncldf1  23241  mretopd  23249  neindisj  23274  neiptopnei  23289  restcls  23338  restntr  23339  ordtbas  23349  cnpnei  23421  cncls2  23430  tgcmp  23558  cmpcld  23559  uncmp  23560  hauscmplem  23563  1stcfb  23602  2ndcctbss  23612  hauspwdom  23658  reftr  23671  comppfsc  23689  kgentopon  23695  ptpjpre1  23728  ptcnplem  23778  txcn  23783  txdis1cn  23792  txhaus  23804  xkopt  23812  imasnopn  23847  imasncld  23848  imasncls  23849  hmeoimaf1o  23927  cmphaushmeo  23957  txhmeo  23960  trfbas2  24000  fbasfip  24025  fbasrn  24041  fmss  24103  elfm2  24105  hauspwpwf1  24144  flfcnp  24161  fclscf  24182  flimfnfcls  24185  fcfval  24190  alexsubALTlem2  24205  alexsubALTlem3  24206  alexsubALTlem4  24207  ptcmplem3  24211  ptcmplem4  24212  cnextfval  24219  cnextcn  24224  tmdgsum2  24253  ustex2sym  24374  neipcfilu  24452  imasdsf1olem  24530  metss2lem  24668  stdbdxmet  24672  stdbdmopn  24675  metrest  24681  metcnp  24698  restmetu  24727  tngngp  24811  icccmplem1  24980  icccvx  25109  evth  25118  lebnumlem1  25120  pi1blem  25198  isncvsngp  25308  equivcau  25459  bcthlem5  25487  cmslssbn  25531  ivthlem3  25612  ovolicc2lem3  25678  ovolicc2lem4  25679  dyaddisj  25755  dyadmbllem  25758  ismbfd  25798  itg2seq  25901  itgss  25971  limciun  26053  dvcobr  26105  dvmptfsum  26134  c1liplem1  26155  c1lip1  26156  lhop  26175  dvcvx  26179  tdeglem4  26217  plyco0  26349  elply2  26353  plypf1  26369  dgreq0  26422  elqaalem2  26481  aalioulem6  26500  aaliou  26501  aaliou2b  26504  ulmss  26560  ulmcn  26562  pserulm  26585  lgamgulmlem5  27197  basellem4  27248  fsumdvdsdiaglem  27347  mpodvdsmulf1o  27358  dvdsmulf1o  27360  chtublem  27375  fsumvma2  27378  logfaclbnd  27386  dchrelbasd  27403  lgsqrlem2  27511  gausslemma2dlem1a  27529  lgseisenlem2  27540  lgsquadlem1  27544  lgsquadlem2  27545  lgsquadlem3  27546  rplogsumlem2  27649  rpvmasumlem  27651  dchrmusum2  27658  dchrvmasumlem1  27659  dchrvmasum2lem  27660  rpvmasum2  27676  dchrisum0lem1  27680  logsqvma  27706  selberg4  27725  pntibndlem3  27756  pntlem3  27773  ostthlem1  27791  ostthlem2  27792  ltsres  27826  nogt01o  27860  oldbdayim  28082  addsproplem2  28163  negsproplem2  28222  mulsval  28302  om2noseqrdg  28497  noseqrdgfn  28499  zmulscld  28590  recut  28687  idmot  28806  brcgr  29250  brbtwn2  29255  axsegconlem8  29274  axpaschlem  29290  axeuclid  29313  axcontlem2  29315  axcontlem7  29320  eengtrkg  29336  upgrex  29442  subgrprop3  29626  subupgr  29637  nbgr0edglem  29706  nb3grprlem1  29730  cusgredg  29774  cusgrres  29798  usgredgsscusgredg  29809  finsumvtxdg2ssteplem4  29898  finsumvtxdg2sstep  29899  wlkl1loop  29987  wlkp1lem4  30024  wwlksnred  30241  wwlksnext  30242  wwlksnextwrd  30246  wpthswwlks2on  30313  clwwlknp  30388  clwwlkel  30397  wwlksext2clwwlk  30408  clwwlknonwwlknonb  30457  3wlkond  30522  1conngr  30545  eucrctshift  30594  fusgr2wsp2nb  30685  numclwwlk1lem2foa  30705  numclwwlk1lem2f1  30708  numclwlk1lem1  30720  numclwlk1lem2  30721  grpoidinvlem1  30856  grporcan  30870  ipblnfi  31207  hvmulcan2  31425  shscli  31669  spansneleq  31922  pjspansn  31929  3oalem2  32015  eigposi  32188  cnlnadjlem2  32420  stlesi  32593  mdslmd1lem1  32677  mdslmd1lem2  32678  cdj1i  32785  disjxpin  32933  nn0xmulclb  33116  xreceu  33241  txomap  34224  pstmxmet  34287  qqhghm  34378  qqhrhm  34379  measinblem  34610  cntmeas  34616  ballotlemsf1o  34904  bnj945  35162  bnj1110  35370  f1resveqaeq  35473  rankfilimbi  35495  cvmopnlem  35770  cvmfolem  35771  cvmliftmolem2  35774  cvmlift2lem10  35804  satf00  35866  satffunlem2lem1  35896  satefvfmla0  35910  mrsubvrs  36014  wzel  36314  btwnconn1lem8  36586  btwnconn1lem9  36587  btwnconn1lem10  36588  btwnconn1lem11  36589  btwnconn1lem12  36590  finminlem  36849  nn0prpwlem  36853  fnessref  36888  refssfne  36889  fnemeet2  36898  consym1  36951  bj-finsumval0  37949  topdifinffinlem  38013  relowlssretop  38029  rdgeqoa  38036  fvineqsneu  38077  pibt2  38083  matunitlindflem1  38287  poimirlem28  38319  mblfinlem1  38328  mblfinlem3  38330  mblfinlem4  38331  ovoliunnfl  38333  mbfresfi  38337  mbfposadd  38338  itg2addnclem2  38343  itg2addnc  38345  ftc1anc  38372  frinfm  38406  fdc  38416  blssp  38427  sstotbnd  38446  isbnd2  38454  ssbnd  38459  prdstotbnd  38465  prdsbnd2  38466  ismtyres  38479  heibor1lem  38480  rrnequiv  38506  rngoisocnv  38652  crngohomfo  38677  pridlc3  38744  membpartlem19  39583  prter3  39676  ax12eq  39735  ax12el  39736  cvratlem  40215  islvol2aN  40386  4atlem4b  40394  4atlem4c  40395  4atlem4d  40396  isline2  40568  isline3  40570  pclfinclN  40744  linepsubclN  40745  pexmidlem4N  40767  diaglbN  41849  dvhvaddcl  41889  dvhvaddcomN  41890  dvhvscacl  41897  djavalN  41929  dibglbN  41960  dihatexv  42132  djhval  42192  mapdrvallem2  42439  evlselvlem  43340  evlselv  43341  mhpind  43346  prjsprellsp  43363  elrfi  43445  nacsfix  43463  eldioph2  43513  lzenom  43521  rexrabdioph  43541  irrapxlem3  43571  pellexlem5  43580  pellex  43582  pell1234qrne0  43600  pell1234qrmulcl  43602  pell14qrdich  43616  pell1qrge1  43617  pellqrex  43626  rmxypairf1o  43658  rmxycomplete  43664  monotoddzzfi  43689  congadd  43713  jm2.19lem3  43738  jm2.19lem4  43739  jm2.25  43746  jm2.26a  43747  jm2.26lem3  43748  expdiophlem1  43768  wepwsolem  43789  lmhmfgsplit  43833  aaitgo  43909  mon1psubm  43946  deg1mhm  43947  succlg  44075  ofoacom  44108  iunrelexp0  44448  isotone2  44795  mnuprdlem4  45005  relpmin  45681  disjrnmpt2  45926  mullimc  46352  mullimcf  46359  climxrre  46484  fprodcncf  46634  stoweidlem17  46751  stoweidlem27  46761  stoweidlem54  46788  fourierdlem42  46883  fourierdlem62  46902  fourierdlem73  46913  fourierdlem76  46916  fourierdlem97  46937  sge0iunmptlemfi  47147  isomenndlem  47264  imarnf1pr  48039  smonoord  48134  fvelsetpreimafv  48156  iccpartiltu  48191  sprsymrelf1lem  48260  prproropf1olem3  48274  paireqne  48280  fmtnoprmfac1  48337  prmdvdsfmtnof1lem2  48357  nprmdvdsfacm1  48396  gricushgr  48702  grimedg  48720  cycl3grtri  48732  gpgedg2iv  48852  pgnbgreunbgrlem2lem1  48899  pgnbgreunbgrlem2lem2  48900  rngcinvALTV  49061  funcringcsetcALTV2lem9  49083  ringcinvALTV  49095  funcringcsetclem9ALTV  49106  lmodvsmdi  49179  lincsum  49229  lindslinindimp2lem4  49261  nn0sumshdiglemB  49420  1arymaptf1  49442  2arymaptf1  49453  dmrnxp  49635  xpco2  49655  initopropd  50041  termopropd  50042  zeroopropd  50043  oduoppcciso  50364  lanpropd  50413  ranpropd  50414