Theorem ad2antrl 716

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 19-Oct-1999.)

Hypothesis

Ref	Expression
ad2ant.1	⊢ (𝜑 → 𝜓)

Assertion

Ref	Expression
ad2antrl	⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Proof of Theorem ad2antrl

Step	Hyp	Ref	Expression
1		ad2ant.1	. . 3 ⊢ (𝜑 → 𝜓)
2	1	adantr 473	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 474	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 387

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 199  df-an 388

This theorem is referenced by:  simprl  759  simprll  767  simprlr  768  simprl1  1199  simprl2  1200  simprl3  1201  disjxiun  4923  reusv2lem4  5152  axprlem5  5181  fr2nr  5382  somin1  5831  tz7.7  6053  f1oprg  6486  soisores  6902  elovmporab1  7210  sorpssi  7272  onint  7325  ordsucelsuc  7352  elxp5  7442  wemoiso  7485  wemoiso2  7486  el2xptp0  7547  ressuppss  7651  imacosuppOLD  7677  tz7.48lem  7879  oalimcl  7986  oeeui  8028  oaabs2  8071  omabs  8073  swoer  8118  ralxpmap  8257  pw2f1olem  8416  enfixsn  8421  mapxpen  8478  mapunen  8481  unxpdomlem2  8517  unxpdomlem3  8518  findcard3  8555  isfinite2  8570  domunfican  8585  fodomfi  8591  fissuni  8623  fipreima  8624  indexfi  8626  fsuppsssupp  8643  marypha1lem  8691  marypha2  8697  supmo  8710  infmo  8753  oieu  8797  brwdom2  8831  ixpiunwdom  8849  cantnfval2  8925  cantnfle  8927  cantnflt  8928  cantnf  8949  wemapwe  8953  cnfcom  8956  rankonidlem  9050  r1pwcl  9069  eldju2ndl  9146  eldju2ndr  9147  djuun  9148  infxpenlem  9232  infxpenc2lem1  9238  fseqenlem1  9243  dfac8clem  9251  mappwen  9331  dfac3  9340  dfac5  9347  dfac12lem3  9364  infunsdom  9433  coftr  9492  ssfin4  9529  domfin4  9530  fin23lem26  9544  fin23lem22  9546  fin23lem28  9559  fin23lem32  9563  fin23lem40  9570  isf32lem5  9576  compssiso  9593  isf34lem4  9596  isfin1-3  9605  fin1a2lem13  9631  hsmexlem2  9646  hsmexlem4  9648  zorn2lem1  9715  ttukeylem6  9733  iundom2g  9759  konigthlem  9787  pwcfsdom  9802  fpwwe2lem12  9860  fpwwe2  9862  pwfseqlem3  9879  winalim2  9915  r1wunlim  9956  inttsk  9993  inar1  9994  grur1  10039  nqereq  10154  ltexprlem7  10261  prlem936  10266  00id  10614  addid2  10622  ltord1  10966  divdiv1  11151  divdiv2  11152  conjmul  11157  ltdivmul  11315  ledivmul  11316  lt2mul2div  11318  ltdiv23  11331  lediv23  11332  lediv12a  11333  ledivp1  11342  negfi  11389  nn0nndivcl  11777  nn0ge0div  11863  peano2uz2  11882  peano5uzi  11883  eluzp1m1  12081  qbtwnre  12408  xralrple  12414  xleadd1a  12461  xmulge0  12492  xmulass  12495  xlemul1a  12496  iooshf  12630  divelunit  12695  eluzgtdifelfzo  12913  modadd1  13090  modmul1  13106  seqcl2  13202  seqfveq2  13206  seqid2  13230  seqhomo  13231  seqdistr  13235  mulexpz  13283  leexp2r  13352  expnlbnd2  13409  expmulnbnd  13410  hashmap  13608  hashfun  13610  hashbclem  13622  hashfacen  13624  hashf1lem2  13626  hashf1  13627  ccatsymb  13744  swrdwrdsymb  13838  swrdsb0eq  13839  ccatpfx  13882  swrdswrd  13886  wrdind  13914  wrdindOLD  13915  wrd2ind  13916  wrd2indOLD  13917  swrdccatin1  13923  swrdccatin2  13928  pfxccatin12lem2  13930  pfxccatin12  13933  swrdccatin12OLD  13934  swrdccat  13937  swrdccatOLD  13938  splidOLD  13967  repswswrd  14002  0csh0  14015  0csh0OLD  14016  2cshw  14036  cshweqrep  14044  relexp0g  14241  relexpsucnnr  14244  relexpindlem  14282  sqrlem1  14462  sqrlem6  14467  rlim  14712  rlimclim1  14762  climsup  14886  caurcvg2  14894  caucvgb  14896  iseralt  14901  sumss  14940  fsum2dlem  14984  mptfzshft  14992  modfsummod  15008  o1fsum  15027  incexclem  15050  divrcnv  15066  flo1  15068  fprodrev  15190  fprod2dlem  15193  ruclem6  15447  moddvds  15477  dvdsaddre2b  15516  dvdsflip  15526  addmodlteqALT  15534  nn0o  15593  fldivndvdslt  15624  bitsf1ocnv  15652  bitsf1  15654  sadcaddlem  15665  bezoutlem2  15743  bezoutlem4  15745  lcmgcdlem  15805  prmind2  15884  isprm5  15906  isprm6  15913  cncongrprm  15924  hashdvds  15967  crth  15970  eulerthlem2  15974  prmdiveq  15978  hashgcdlem  15980  hashgcdeq  15981  iserodd  16027  pclem  16030  pcprendvds2  16033  pcexp  16051  pcneg  16065  pc2dvds  16070  pcmpt  16083  prmpwdvds  16095  pockthg  16097  prmreclem5  16111  4sqlem11  16146  ramub2  16205  ramubcl  16209  ram0  16213  ramub1lem2  16218  ramcl  16220  prmgaplem3  16244  prmgaplem6  16247  setscom  16382  sscpwex  16956  initoeu2  17147  setcinv  17221  funcestrcsetclem9  17269  funcsetcestrclem9  17284  fullsetcestrc  17287  1stfcl  17318  2ndfcl  17319  hofpropd  17388  isacs3lem  17647  isacs4lem  17649  acsmap2d  17660  submnd0  17801  subsubm  17838  frmdup1  17883  frmdup3lem  17885  sgrp2nmndlem2  17893  isgrpinv  17956  subsubg  18099  cycsubgcl  18102  conjghm  18173  qusghm  18179  gsumwrev  18278  symgfixelsi  18337  symgsssg  18369  symgfisg  18370  psgnunilem2  18398  odf1o2  18472  sylow1lem1  18497  odcau  18503  pgpfi  18504  pgpssslw  18513  fislw  18524  efgtlen  18623  efginvrel2  18624  efgrelexlemb  18649  efgredeu  18651  efgcpbllemb  18654  frgpup1  18674  cygabl  18778  lt6abl  18782  gsum2d  18858  gsum2d2lem  18859  gsum2d2  18860  telgsumfzslem  18871  dmdprdsplit2lem  18930  ablfacrp  18951  pgpfac1lem3  18962  gsummgp0  19094  irredrmul  19193  subsubrg  19297  islss4  19469  lspextmo  19563  lspsnat  19652  issubassa  19831  resspsradd  19923  resspsrmul  19924  coe1tmmul2  20163  pf1ind  20236  prmirredlem  20358  znf1o  20416  znidomb  20426  frgpcyg  20438  psgnghm  20442  psgndiflemB  20462  frlmlbs  20659  frlmup1  20660  lindfind  20678  islindf3  20688  lindfmm  20689  mamulid  20770  mat1dimelbas  20800  mdetdiaglem  20927  mdetralt2  20938  mndifsplit  20965  smadiadetglem2  21001  1elcpmat  21043  pmatcollpw3lem  21111  chfacfisf  21182  chfacfisfcpmat  21183  chfacffsupp  21184  chfacfscmulfsupp  21187  chfacfscmulgsum  21188  chfacfpmmulfsupp  21191  chfacfpmmulgsum  21192  chfacfpmmulgsum2  21193  cayhamlem1  21194  cpmadugsumlemF  21204  cayleyhamilton1  21220  tgcl  21297  pptbas  21336  clsval2  21378  mretopd  21420  lmbr2  21587  cncls2  21601  nrmsep  21685  regsep2  21704  cmpsublem  21727  cmpsub  21728  tgcmp  21729  uncmp  21731  hauscmplem  21734  iunconnlem  21755  1stcrest  21781  2ndcctbss  21783  2ndcsep  21787  dis2ndc  21788  hausllycmp  21822  dislly  21825  kgentopon  21866  1stckgen  21882  kgencn3  21886  ptpjpre1  21899  ptbasin  21905  ptpjopn  21940  dfac14  21946  ptcnplem  21949  txcn  21954  txindis  21962  txdis1cn  21963  ptrescn  21967  txcmplem1  21969  txcmp  21971  txhaus  21975  txlm  21976  tx1stc  21978  txkgen  21980  xkococn  21988  qtopcn  22042  kqreglem1  22069  kqreglem2  22070  kqnrmlem1  22071  kqnrmlem2  22072  hmeoimaf1o  22098  reghmph  22121  nrmhmph  22122  txhmeo  22131  ptuncnv  22135  filconn  22211  fbasrn  22212  fmfnfmlem2  22283  flimfnfcls  22356  cnpfcfi  22368  alexsublem  22372  alexsubALTlem2  22376  alexsubALTlem3  22377  alexsubALTlem4  22378  alexsubALT  22379  ptcmplem3  22382  cnextfval  22390  tsmsxp  22482  imasdsf1olem  22702  bl2in  22729  blssps  22753  blss  22754  blssexps  22755  blssex  22756  blcld  22834  stdbdxmet  22844  met1stc  22850  prdsxmslem2  22858  metcnp3  22869  metcnpi3  22875  txmetcnp  22876  nmo0  23063  nmoid  23070  icccmplem1  23149  icccmp  23152  xrge0tsms  23161  metdseq0  23181  cnheiborlem  23277  cnheibor  23278  cnllycmp  23279  pcoval2  23339  cmetcaulem  23610  iscmet3lem1  23613  iscmet3lem2  23614  equivcau  23622  lmcau  23635  cncmet  23644  ivthlem2  23772  ivthlem3  23773  ovoliunlem2  23823  ovolscalem2  23834  uniioombl  23909  dyaddisj  23916  opnmbllem  23921  volivth  23927  ismbfd  23959  ismbf3d  23974  mbfimaopnlem  23975  mbfinf  23985  itg1addlem4  24019  mbfi1fseqlem1  24035  mbfi1fseqlem3  24037  mbfi1fseqlem4  24038  mbfi1fseqlem5  24039  mbfi1fseqlem6  24040  itg2seq  24062  itg2lea  24064  itg2split  24069  itg2cnlem1  24081  limciun  24211  dvmptfsum  24291  rolle  24306  c1lip1  24313  dvcnvrelem1  24333  dvcnvre  24335  dvcvx  24336  itgsubst  24365  tdeglem4  24373  mdegmullem  24391  plyco0  24501  coemullem  24559  dgreq0  24574  dgrmul  24579  dgrco  24584  elqaalem2  24628  aannenlem1  24636  aaliou3lem9  24658  ulmres  24695  ulmshftlem  24696  angneg  25098  dcubic  25141  cxploglim  25273  cxploglim2  25274  scvxcvx  25281  lgamgulmlem5  25328  lgamcvg2  25350  ftalem2  25369  basellem3  25378  basellem4  25379  sqff1o  25477  fsumdvdsdiaglem  25478  dvdsflsumcom  25483  dvdsmulf1o  25489  fsumvma2  25508  logfac2  25511  logfacrlim  25518  logexprlim  25519  dchrelbasd  25533  lgsne0  25629  lgsqrlem2  25641  lgsqrmodndvds  25647  gausslemma2dlem1a  25659  lgseisenlem2  25670  lgsquadlem1  25674  lgsquadlem2  25675  lgsquadlem3  25676  lgsquad2lem2  25679  2sqlem8  25720  2sqlem11  25723  2sqreultlem  25741  2sqreunnltlem  25744  chpo1ubb  25775  vmadivsum  25776  rplogsumlem2  25779  rpvmasumlem  25781  dchrmusum2  25788  dchrvmasumlem1  25789  dchrisum0fno1  25805  dchrisum0re  25807  dchrisum0lem1  25810  dchrisum0lem2  25812  dchrisum0lem3  25813  dchrisum0  25814  mulogsumlem  25825  mulog2sumlem2  25829  vmalogdivsum2  25832  logsqvma  25836  log2sumbnd  25838  selberglem3  25841  selberg  25842  selberg2lem  25844  selberg2b  25846  selberg3lem2  25852  pntrmax  25858  pntrsumo1  25859  pntlemn  25894  pntlemp  25904  qabvle  25919  ostthlem1  25921  ostthlem2  25922  ostth2lem2  25928  ostth3  25932  idmot  26041  brbtwn2  26410  colinearalglem4  26414  colinearalg  26415  ax5seglem9  26442  axpaschlem  26445  axcontlem2  26470  axcontlem7  26475  axcontlem8  26476  eengtrkg  26491  upgr1eopALT  26621  uspgredg2vlem  26724  subumgr  26789  nbgr0vtxlem  26856  edgnbusgreu  26868  nb3grprlem1  26881  wlkl1loop  27138  pthdivtx  27234  usgr2pth  27269  crctcshwlkn0  27323  wlklnwwlkln1  27370  wwlksnext  27397  clwwlkccatlem  27511  clwlkclwwlklem2a  27520  clwwlkinwwlk  27571  clwwlkinwwlkOLD  27572  clwwlkn1loopb  27575  clwwlkfOLD  27580  clwwlkf  27585  wwlksubclwwlk  27597  wwlksubclwwlkOLD  27598  clwwlknscsh  27602  clwwlknon1  27641  1conngr  27739  n4cyclfrgr  27841  numclwwlk2lem1lem  27892  2clwwlk2clwwlk  27903  2clwwlk2clwwlkOLD  27904  numclwwlk1lem2f1  27915  numclwwlk1lem2f1OLD  27920  numclwlk1lem1  27938  numclwwlk2lem1  27945  numclwlk2lem2f  27946  numclwlk2lem2fOLD  27949  numclwwlk7  27964  frgrogt3nreg  27970  grpoidinvlem1  28074  grpoidinvlem3  28076  grporcan  28088  nmlnoubi  28366  blocnilem  28374  ipblnfi  28426  htthlem  28489  ocsh  28857  shmodsi  28963  pjhthlem2  28966  5oalem2  29229  eigposi  29410  nmopub2tALT  29483  nmfnleub2  29500  nmcexi  29600  nmopcoi  29669  kbass3  29692  mdslmd1lem1  29899  mdslmd1lem2  29900  chirredlem2  29965  chirredlem4  29967  mdsymlem3  29979  mdsymlem5  29981  sumdmdii  29989  sumdmdlem  29992  sumdmdlem2  29993  foresf1o  30060  disjxpin  30122  1stpreimas  30218  resf1o  30243  nn0xmulclb  30273  wrdt2ind  30393  gsumvsca1  30558  gsumvsca2  30559  xrge0tsmsd  30563  islinds5  30638  mdetpmtr1  30763  mdetpmtr2  30764  pstmxmet  30814  qqhghm  30906  qqhrhm  30907  esumpcvgval  31014  volmeas  31168  imambfm  31198  dya2iocnrect  31217  oddpwdc  31290  sseqf  31329  orvcgteel  31404  orvclteel  31409  ballotlemsf1o  31450  bnj1110  31932  bnj1118  31934  txpconn  32097  connpconn  32100  cnllysconn  32110  rellysconn  32116  cvmsss2  32139  cvmlift2lem9  32176  satf00  32217  fmlasuc  32229  mrsubfval  32308  mppsval  32372  dfon2lem6  32586  trpredmintr  32624  wzel  32665  fprlem1  32691  frrlem15  32696  sltres  32723  nosupno  32757  nosupbnd2  32770  sslttr  32822  ifscgr  33059  cgrxfr  33070  btwnconn1lem5  33106  btwnconn1lem6  33107  btwnconn1lem12  33113  brsegle  33123  finminlem  33220  nn0prpwlem  33224  fnessref  33259  refssfne  33260  neibastop1  33261  topjoin  33267  fnemeet2  33269  bj-finsumval0  34063  topdifinffinlem  34103  lindsadd  34359  matunitlindflem2  34363  poimirlem28  34394  poimirlem32  34398  opnmbllem0  34402  mblfinlem1  34403  mblfinlem4  34406  ismblfin  34407  mbfresfi  34412  itg2addnclem  34417  itg2addnclem3  34419  itg2addnc  34420  bddiblnc  34436  unirep  34463  frinfm  34485  sdclem2  34492  geomcau  34509  istotbnd3  34524  sstotbnd2  34527  sstotbnd  34528  sstotbnd3  34529  totbndbnd  34542  cntotbnd  34549  ismtyres  34561  heibor1lem  34562  heiborlem1  34564  heiborlem8  34571  ismndo1  34626  isdivrngo  34703  unichnidl  34784  erim2  35389  cvlcvr1  35953  ishlat3N  35968  llnmlplnN  36153  islvol2aN  36206  4atlem4c  36215  4atlem4d  36216  isline2  36388  isline3  36390  linepsubclN  36565  lhpexle3lem  36625  lhpjat2  36635  cdlemd4  36815  cdleme0cq  36829  cdleme32fva  37051  cdleme32fvaw  37053  tendo0mul  37440  tendo0mulr  37441  diameetN  37670  dvhvaddcl  37709  dvhvaddcomN  37710  cdlemm10N  37732  dvadiaN  37742  djavalN  37749  dihvalcqat  37853  dihopelvalcpre  37862  djhval  38012  dihjat1lem  38042  prjspertr  38696  prjsprellsp  38702  elrfi  38720  nacsfix  38738  fzsplit1nn0  38780  eldioph2  38788  lzenom  38796  irrapxlem3  38851  pellexlem5  38860  pell1234qrne0  38880  pell1234qrmulcl  38882  pell14qrdich  38896  pell1qrge1  38897  pellqrex  38906  reglogltb  38918  reglogleb  38919  rmxypairf1o  38938  rmxycomplete  38944  monotoddzzfi  38969  congadd  38993  congsym  38995  acongrep  39007  jm2.19lem3  39018  jm2.19lem4  39019  jm2.22  39022  jm2.25  39026  expdiophlem1  39048  wepwsolem  39072  kelac1  39093  lmhmfgsplit  39116  pwslnm  39124  hbtlem6  39159  hbt  39160  mon1psubm  39236  deg1mhm  39237  iunrelexp0  39444  dssmapnvod  39763  gsumws3  39948  gsumws4  39949  mulltgt0  40732  fnchoice  40739  disjrnmpt2  40904  fzisoeu  41026  fsumiunss  41317  climinf  41348  mullimc  41358  mullimcf  41365  stoweidlem14  41760  stoweidlem17  41763  stoweidlem34  41780  stoweidlem50  41796  fourierdlem42  41895  fourierdlem62  41914  fourierdlem71  41923  fourierdlem76  41928  qndenserrnbllem  42040  subsaliuncl  42102  sge0resplit  42149  2reu8i  42748  iccpartigtl  42985  prproropf1olem2  43064  prproropf1olem4  43066  paireqne  43071  prmdvdsfmtnof1lem2  43145  bgoldbtbndlem3  43370  bgoldbtbnd  43372  isomushgr  43389  isomuspgrlem2c  43393  uspgrsprf1  43420  subsubmgm  43462  isassintop  43511  2zlidl  43599  2zrngnmrid  43615  rngcinv  43646  rngcinvALTV  43658  ringcinv  43697  funcringcsetcALTV2lem9  43709  ringcinvALTV  43721  funcringcsetclem9ALTV  43732  fldhmsubc  43749  fldhmsubcALTV  43767  mndpsuppss  43815  gsumlsscl  43827  lincsum  43881  lindslinindsimp1  43909  lindslinindimp2lem4  43913  lincresunitlem2  43928  elfzolborelfzop1  43972  elbigo2  44010  digexp  44065  dig1  44066  nn0sumshdiglemB  44078  itschlc0xyqsol  44152