Theorem ad2antrl 741

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	adantl 487	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	adantrr 730	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:  simprl  783  simprll  791  simprlr  792  simprl1  1237  simprl2  1238  simprl3  1239  disjxiun  5100  reusv2lem4  5366  axprlem5OLD  5396  fr2nr  5632  somin1  6127  tz7.7  6383  f1oprg  6865  f1resveqaeq  7271  soisores  7329  elovmporab1w  7662  elovmporab1  7663  sorpssi  7731  onint  7790  ordsucelsuc  7819  elxp5  7921  resf1extb  7932  f1oabexg  7939  wemoiso  7971  wemoiso2  7972  el2xptp0  8034  mpof1o2d  8124  frxp2  8143  frxp3  8150  ressuppss  8182  fprlem1  8300  tz7.48lemOLD  8433  oalimcl  8550  oeeui  8593  nnaordex2  8630  oaabs2  8640  omabs  8642  swoer  8731  ralxpmap  8906  pw2f1olem  9082  enfixsn  9087  mapxpen  9144  mapunen  9147  php  9204  unxpdomlem2  9230  unxpdomlem3  9231  isfinite2  9271  fodomfi  9285  domunfican  9294  fissuni  9327  fipreima  9328  indexfi  9330  fsuppsssupp  9354  marypha1lem  9406  marypha2  9412  supmo  9425  infmo  9470  oieu  9514  brwdom2  9548  ixpiunwdom  9565  cantnfval2  9651  cantnfle  9653  cantnflt  9654  cantnf  9675  wemapwe  9679  cnfcom  9682  frrlem15  9742  rankonidlem  9813  r1pwcl  9832  eldju2ndl  9932  eldju2ndr  9933  djuun  9934  infxpenlem  10019  infxpenc2lem1  10025  fseqenlem1  10030  dfac8clem  10038  mappwen  10118  dfac3  10127  dfac5  10134  dfac12lem3  10151  infunsdom  10218  coftr  10278  ssfin4  10315  domfin4  10316  fin23lem26  10330  fin23lem22  10332  fin23lem28  10345  fin23lem32  10349  fin23lem40  10356  isf32lem5  10362  compssiso  10379  isf34lem4  10382  isfin1-3  10391  fin1a2lem13  10417  hsmexlem2  10432  hsmexlem4  10434  zorn2lem1  10501  ttukeylem6  10519  iundom2g  10551  konigthlem  10580  pwcfsdom  10595  fpwwe2lem11  10653  fpwwe2  10655  pwfseqlem3  10672  winalim2  10708  r1wunlim  10749  inttsk  10786  inar1  10787  grur1  10832  nqereq  10947  ltexprlem7  11054  prlem936  11059  00id  11412  addlid  11420  ltord1  11767  divdiv1  11953  divdiv2  11954  conjmul  11959  ltdivmul  12117  ledivmul  12118  lt2mul2div  12120  ltdiv23  12133  lediv23  12134  lediv12a  12135  ledivp1  12144  negfi  12191  nn0nndivcl  12603  nn0ge0div  12693  peano2uz2  12712  peano5uzi  12713  eluzp1m1  12916  qbtwnre  13254  xralrple  13260  xleadd1a  13308  xmulge0  13339  xmulass  13342  xlemul1a  13343  iooshf  13482  divelunit  13550  eluzgtdifelfzo  13786  modadd1  13972  modmul1  13991  seqcl2  14087  seqfveq2  14091  seqid2  14115  seqhomo  14116  seqdistr  14120  mulexpz  14169  leexp2r  14241  expnlbnd2  14301  expmulnbnd  14302  hashmap  14503  hashfun  14505  hashbclem  14520  hashfacen  14522  hashf1lem2  14524  hashf1  14525  ccatsymb  14651  swrdwrdsymb  14735  swrdsb0eq  14736  ccatpfx  14773  swrdswrd  14777  wrdind  14794  wrd2ind  14795  swrdccatin1  14797  swrdccatin2  14801  pfxccatin12lem2  14803  pfxccatin12  14805  swrdccat  14807  repswswrd  14858  0csh0  14867  cshwidxmod  14877  2cshw  14887  cshweqrep  14895  relexp0g  15098  relexpsucnnr  15101  relexpindlem  15139  01sqrexlem1  15332  01sqrexlem6  15337  rlim  15585  rlimclim1  15635  climsup  15760  caurcvg2  15768  caucvgb  15770  iseralt  15775  sumss  15813  fsum2dlem  15859  mptfzshft  15867  modfsummod  15884  o1fsum  15903  incexclem  15928  divrcnv  15944  flo1  15946  fprodrev  16067  fprod2dlem  16070  ruclem6  16326  moddvds  16356  dvdsaddre2b  16400  dvdsflip  16410  addmodlteqALT  16418  nn0o  16476  fldivndvdslt  16509  bitsf1ocnv  16537  bitsf1  16539  sadcaddlem  16550  bezoutlem2  16633  bezoutlem4  16635  lcmgcdlem  16699  prmind2  16778  isprm5  16801  isprm6  16808  prmdvdsncoprmbd  16821  cncongrprm  16823  hashdvds  16869  crth  16872  eulerthlem2  16876  prmdiveq  16880  hashgcdlem  16882  hashgcdeq  16884  iserodd  16930  pclem  16933  pcprendvds2  16936  pcexp  16954  pcneg  16969  pc2dvds  16974  pcmpt  16987  prmpwdvds  16999  pockthg  17001  prmreclem5  17015  4sqlem11  17050  ramub2  17109  ramubcl  17113  ram0  17117  ramub1lem2  17122  ramcl  17124  prmgaplem3  17148  prmgaplem6  17151  setscom  17275  sscpwex  17907  initoeu2  18108  setcinv  18182  funcestrcsetclem9  18239  funcsetcestrclem9  18254  fullsetcestrc  18257  1stfcl  18288  2ndfcl  18289  hofpropd  18358  isacs3lem  18633  isacs4lem  18635  acsmap2d  18646  chnflenfi  18719  subsubmgm  18815  submnd0OLD  18873  mndpsuppss  18875  subsubm  18928  insubm  18930  frmdup1  18976  frmdup3lem  18978  sgrp2nmndlem2  19039  isgrpinv  19120  subsubg  19276  cycsubgcl  19337  conjghm  19379  qusghm  19385  gsumwrev  19496  gsmsymgrfixlem1  19557  symgfixelsi  19565  symgsssg  19597  symgfisg  19598  psgnunilem2  19625  odf1o2  19703  sylow1lem1  19728  odcau  19734  pgpfi  19735  pgpssslw  19744  fislw  19755  efgtlen  19856  efginvrel2  19857  efgrelexlemb  19880  efgredeu  19882  efgcpbllemb  19885  frgpup1  19905  lt6abl  20025  gsum2d  20102  gsum2d2lem  20103  gsum2d2  20104  telgsumfzslem  20118  dmdprdsplit2lem  20177  ablfacrp  20198  pgpfac1lem3  20209  gsummgp0  20461  irredrmul  20571  subsubrng  20728  subsubrg  20763  rngcinv  20802  ringcinv  20836  fldhmsubc  20954  islss4  21149  lspextmo  21243  lspsnat  21335  prmirredlem  21688  znf1o  21767  znidomb  21777  frgpcyg  21789  psgnghm  21796  psgndiflemB  21816  frlmlbs  22013  frlmup1  22014  lindfind  22032  islindf3  22042  lindfmm  22043  issubassa3  22084  resspsradd  22192  resspsrmul  22193  psdmul  22397  coe1tmmul2  22505  pf1ind  22583  mamulid  22666  mat1dimelbas  22696  mdetdiaglem  22823  mdetralt2  22834  mndifsplit  22861  smadiadetglem2  22897  matunitlindflem2  22905  1elcpmat  22943  pmatcollpw3lem  23011  chfacfisf  23082  chfacfisfcpmat  23083  chfacffsupp  23084  chfacfscmulfsupp  23087  chfacfscmulgsum  23088  chfacfpmmulfsupp  23091  chfacfpmmulgsum  23092  chfacfpmmulgsum2  23093  cayhamlem1  23094  cpmadugsumlemF  23104  cayleyhamilton1  23120  tgcl  23197  pptbas  23236  clsval2  23278  mretopd  23320  lmbr2  23487  cncls2  23501  nrmsep  23585  regsep2  23604  cmpsublem  23627  cmpsub  23628  tgcmp  23629  uncmp  23631  hauscmplem  23634  iunconnlem  23655  1stcrest  23681  2ndcctbss  23684  2ndcsep  23688  dis2ndc  23689  hausllycmp  23723  dislly  23726  kgentopon  23767  1stckgen  23783  kgencn3  23787  ptpjpre1  23800  ptbasin  23806  ptpjopn  23841  dfac14  23847  ptcnplem  23850  txcn  23855  txindis  23863  txdis1cn  23864  ptrescn  23868  txcmplem1  23870  txcmp  23872  txhaus  23876  txlm  23877  tx1stc  23879  txkgen  23881  xkococn  23889  qtopcn  23943  kqreglem1  23970  kqreglem2  23971  kqnrmlem1  23972  kqnrmlem2  23973  hmeoimaf1o  23999  reghmph  24022  nrmhmph  24023  txhmeo  24032  ptuncnv  24036  filconn  24112  fbasrn  24113  fmfnfmlem2  24184  flimfnfcls  24257  cnpfcfi  24269  alexsublem  24273  alexsubALTlem2  24277  alexsubALTlem3  24278  alexsubALTlem4  24279  alexsubALT  24280  ptcmplem3  24283  cnextfval  24291  tsmsxp  24384  imasdsf1olem  24602  bl2in  24629  blssps  24653  blss  24654  blssexps  24655  blssex  24656  blcld  24734  stdbdxmet  24744  met1stc  24750  prdsxmslem2  24758  metcnp3  24769  metcnpi3  24775  txmetcnp  24776  nmo0  24964  nmoid  24971  icccmplem1  25052  icccmp  25055  xrge0tsms  25064  metdseq0  25084  cnheiborlem  25185  cnheibor  25186  cnllycmp  25187  pcoval2  25247  cmetcaulem  25519  iscmet3lem1  25522  iscmet3lem2  25523  equivcau  25531  lmcau  25544  cncmet  25553  ivthlem2  25683  ivthlem3  25684  ovoliunlem2  25734  ovolscalem2  25745  uniioombl  25820  dyaddisj  25827  opnmbllem  25832  volivth  25838  ismbfd  25870  ismbf3d  25885  mbfimaopnlem  25886  mbfinf  25896  itg1addlem4  25930  mbfi1fseqlem1  25946  mbfi1fseqlem3  25948  mbfi1fseqlem4  25949  mbfi1fseqlem5  25950  mbfi1fseqlem6  25951  itg2seq  25973  itg2lea  25975  itg2split  25980  itg2cnlem1  25992  bddiblnc  26072  limciun  26124  dvmptfsum  26205  rolle  26220  c1lip1  26227  dvcnvrelem1  26247  dvcnvre  26249  dvcvx  26250  itgsubst  26279  tdeglem4  26288  mdegmullem  26306  plyco0  26420  coemullem  26479  dgreq0  26494  dgrmul  26499  dgrco  26504  elqaalem2  26555  preimaaa  26558  aannenlem1  26567  aaliou3lem9  26589  ulmres  26627  ulmshftlem  26628  angneg  27043  dcubic  27086  cxploglim  27217  cxploglim2  27218  scvxcvx  27225  lgamgulmlem5  27272  lgamcvg2  27294  ftalem2  27313  basellem3  27322  basellem4  27323  sqff1o  27421  fsumdvdsdiaglem  27422  dvdsflsumcom  27427  mpodvdsmulf1o  27433  dvdsmulf1o  27435  fsumvma2  27453  logfac2  27456  logfacrlim  27463  logexprlim  27464  dchrelbasd  27478  lgsne0  27574  lgsqrlem2  27586  lgsqrmodndvds  27592  gausslemma2dlem1a  27604  lgseisenlem2  27615  lgsquadlem1  27619  lgsquadlem2  27620  lgsquadlem3  27621  lgsquad2lem2  27624  2sqlem8  27665  2sqlem11  27668  2sqreultlem  27686  2sqreunnltlem  27689  chpo1ubb  27720  vmadivsum  27721  rplogsumlem2  27724  rpvmasumlem  27726  dchrmusum2  27733  dchrvmasumlem1  27734  dchrisum0fno1  27750  dchrisum0re  27752  dchrisum0lem1  27755  dchrisum0lem2  27757  dchrisum0lem3  27758  dchrisum0  27759  mulogsumlem  27770  mulog2sumlem2  27774  vmalogdivsum2  27777  logsqvma  27781  log2sumbnd  27783  selberglem3  27786  selberg  27787  selberg2lem  27789  selberg2b  27791  selberg3lem2  27797  pntrmax  27803  pntrsumo1  27804  pntlemn  27839  pntlemp  27849  qabvle  27864  ostthlem1  27866  ostthlem2  27867  ostth2lem2  27873  ostth3  27877  ltsres  27901  nosupno  27942  nosupbnd2  27955  noinfno  27957  noinfbnd2  27970  etaslts  28061  cuteq1  28085  addsproplem2  28238  mulsval  28377  precsexlem11  28485  n0fincut  28623  zmulscld  28665  bdayfinbndlem1  28735  idmot  28882  plngval  29137  brbtwn2  29365  colinearalglem4  29369  colinearalg  29370  ax5seglem9  29397  axpaschlem  29400  axcontlem2  29425  axcontlem7  29430  axcontlem8  29431  eengtrkg  29446  upgr1eopALT  29577  uspgredg2vlem  29686  subumgr  29751  nbgr0edglem  29819  edgnbusgreu  29830  nb3grprlem1  29843  wlkl1loop  30100  pthdivtx  30194  usgr2pth  30232  crctcshwlkn0  30292  wlklnwwlkln1  30339  wwlksnext  30364  clwwlkccatlem  30462  clwlkclwwlklem2a  30471  clwwlkinwwlk  30513  clwwlkn1loopb  30516  clwwlkf  30520  wwlksext2clwwlk  30530  wwlksubclwwlk  30531  clwwlknscsh  30535  clwwlknon1  30570  clwwlknonex2e  30583  1conngr  30677  n4cyclfrgr  30774  numclwwlk2lem1lem  30825  2clwwlk2clwwlk  30833  numclwwlk1lem2f1  30840  numclwlk1lem1  30852  numclwwlk2lem1  30859  numclwlk2lem2f  30860  numclwwlk7  30874  frgrogt3nreg  30880  grpoidinvlem1  30988  grpoidinvlem3  30990  grporcan  31002  nmlnoubi  31280  blocnilem  31288  ipblnfi  31339  htthlem  31401  ocsh  31767  shmodsi  31873  pjhthlem2  31876  5oalem2  32139  eigposi  32320  nmopub2tALT  32393  nmfnleub2  32410  nmcexi  32510  nmopcoi  32579  kbass3  32602  mdslmd1lem1  32809  mdslmd1lem2  32810  chirredlem2  32875  chirredlem4  32877  mdsymlem3  32889  mdsymlem5  32891  sumdmdii  32899  sumdmdlem  32902  sumdmdlem2  32903  foresf1o  32982  disjxpin  33064  1stpreimas  33181  resf1o  33204  nn0xmulclb  33245  wrdt2ind  33398  xrge0tsmsd  33516  gsumvsca1  33669  gsumvsca2  33670  islinds5  33805  1arithidomlem2  33949  mplvrpmmhm  34059  irngnzply1  34204  mdetpmtr1  34336  mdetpmtr2  34337  pstmxmet  34410  qqhghm  34501  qqhrhm  34502  esumpcvgval  34591  volmeas  34745  imambfm  34776  dya2iocnrect  34795  oddpwdc  34868  sseqf  34906  orvcgteel  34982  orvclteel  34987  ballotlemsf1o  35028  bnj1110  35494  bnj1118  35496  txpconn  35814  connpconn  35817  cnllysconn  35827  rellysconn  35833  cvmsss2  35856  cvmlift2lem9  35893  satf00  35956  fmlasuc  35968  mrsubfval  36090  mppsval  36154  dfon2lem6  36368  wzel  36404  ifscgr  36627  cgrxfr  36638  btwnconn1lem5  36674  btwnconn1lem6  36675  btwnconn1lem12  36681  brsegle  36691  finminlem  36940  nn0prpwlem  36944  fnessref  36979  refssfne  36980  neibastop1  36981  topjoin  36987  fnemeet2  36989  weiunse  37090  bj-prmoore  37868  bj-finsumval0  38040  topdifinffinlem  38104  lindsadd  38370  poimirlem28  38400  poimirlem32  38404  opnmbllem0  38408  mblfinlem1  38409  mblfinlem4  38412  ismblfin  38413  mbfresfi  38418  itg2addnclem  38423  itg2addnclem3  38425  itg2addnc  38426  unirep  38467  frinfm  38488  sdclem2  38495  geomcau  38512  istotbnd3  38524  sstotbnd2  38527  sstotbnd  38528  sstotbnd3  38529  totbndbnd  38542  cntotbnd  38549  ismtyres  38561  heibor1lem  38562  heiborlem1  38564  heiborlem8  38571  ismndo1  38626  isdivrngo  38703  unichnidl  38784  erimeq2  39514  cvlcvr1  40215  ishlat3N  40230  llnmlplnN  40415  islvol2aN  40468  4atlem4c  40477  4atlem4d  40478  isline2  40650  isline3  40652  linepsubclN  40827  lhpexle3lem  40887  lhpjat2  40897  cdlemd4  41077  cdleme0cq  41091  cdleme32fva  41313  cdleme32fvaw  41315  tendo0mul  41702  tendo0mulr  41703  diameetN  41932  dvhvaddcl  41971  dvhvaddcomN  41972  cdlemm10N  41994  dvadiaN  42004  djavalN  42011  dihvalcqat  42115  dihopelvalcpre  42124  djhval  42274  dihjat1lem  42304  sticksstones11  43025  sticksstones22  43037  remul01  43285  zaddcom  43355  zmulcom  43359  fidomncyc  43420  evlselvlem  43437  evlselv  43438  fsuppind  43439  mhpind  43443  prjspertr  43454  prjsprellsp  43460  elrfi  43542  nacsfix  43560  fzsplit1nn0  43602  eldioph2  43610  lzenom  43618  irrapxlem3  43668  pellexlem5  43677  pell1234qrne0  43697  pell1234qrmulcl  43699  pell14qrdich  43713  pell1qrge1  43714  pellqrex  43723  reglogltb  43735  reglogleb  43736  rmxypairf1o  43755  rmxycomplete  43761  monotoddzzfi  43786  congadd  43810  congsym  43812  acongrep  43824  jm2.19lem3  43835  jm2.19lem4  43836  jm2.22  43839  jm2.25  43843  expdiophlem1  43865  wepwsolem  43886  kelac1  43907  lmhmfgsplit  43930  pwslnm  43938  hbtlem6  43973  hbt  43974  mon1psubm  44043  deg1mhm  44044  omord2lim  44144  succlg  44172  onmcl  44175  ofoafo  44200  ofoacom  44205  fzunt  44298  fzuntd  44299  fzunt1d  44300  fzuntgd  44301  iunrelexp0  44545  dssmapnvod  44863  gsumws3  45039  gsumws4  45040  mulltgt0  45859  fnchoice  45866  disjrnmpt2  46023  fzisoeu  46136  fsumiunss  46408  climinf  46439  mullimc  46449  mullimcf  46456  stoweidlem14  46845  stoweidlem17  46848  stoweidlem34  46865  stoweidlem50  46881  fourierdlem42  46980  fourierdlem62  46999  fourierdlem71  47008  fourierdlem76  47013  qndenserrnbllem  47125  subsaliuncl  47189  sge0resplit  47237  3f1oss1  47966  2reu8i  48004  addmodne  48241  fundcmpsurinjpreimafv  48311  iccpartigtl  48326  prproropf1olem2  48407  prproropf1olem4  48409  paireqne  48414  prmdvdsfmtnof1lem2  48491  nprmdvdsfacm1  48530  bgoldbtbndlem3  48726  bgoldbtbnd  48728  grimcnv  48807  gricushgr  48836  cycldlenngric  48847  grimedg  48854  grtrimap  48867  isubgr3stgrlem6  48890  isubgr3stgrlem7  48891  isubgr3stgrlem8  48892  isubgr3stgrlem9  48893  grlimfn  48898  gpgedg2iv  48986  gpg5nbgrvtx03starlem2  48988  gpg5nbgrvtx13starlem2  48991  uspgrsprf1  49066  isassintop  49128  2zlidl  49158  2zrngnmrid  49174  rngcinvALTV  49194  funcringcsetcALTV2lem9  49216  ringcinvALTV  49228  funcringcsetclem9ALTV  49239  fldhmsubcALTV  49251  gsumlsscl  49313  lincsum  49362  lindslinindsimp1  49390  lindslinindimp2lem4  49394  lincresunitlem2  49409  elfzolborelfzop1  49452  elbigo2  49485  digexp  49540  dig1  49541  nn0sumshdiglemB  49553  1arymaptf1  49575  2arymaptf1  49586  itcoval1  49596  itcoval2  49597  itcoval3  49598  itcovalsucov  49601  ackvalsuc1mpt  49611  itschlc0xyqsol  49700  brab2dd  49759  dmrnxp  49768  xpco2  49788  initopropd  50172  termopropd  50173  zeroopropd  50174  prcofpropd  50308  thincciso  50382  indthinc  50391  indthincALT  50392  oduoppcciso  50495  lanpropd  50544  ranpropd  50545