Theorem ad2antrl 728

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  simprl  771  simprll  779  simprlr  780  simprl1  1219  simprl2  1220  simprl3  1221  disjxiun  5140  reusv2lem4  5401  axprlem5OLD  5430  fr2nr  5662  somin1  6153  tz7.7  6410  f1oprg  6893  soisores  7347  elovmporab1w  7680  elovmporab1  7681  sorpssi  7749  onint  7810  ordsucelsuc  7842  elxp5  7945  resf1extb  7956  f1oabexg  7964  wemoiso  7998  wemoiso2  7999  el2xptp0  8061  frxp2  8169  frxp3  8176  ressuppss  8208  fprlem1  8325  tz7.48lem  8481  oalimcl  8598  oeeui  8640  nnaordex2  8677  oaabs2  8687  omabs  8689  swoer  8776  ralxpmap  8936  pw2f1olem  9116  enfixsn  9121  mapxpen  9183  mapunen  9186  php  9247  unxpdomlem2  9287  unxpdomlem3  9288  findcard3OLD  9319  isfinite2  9334  fodomfi  9350  domunfican  9361  fodomfiOLD  9370  fissuni  9397  fipreima  9398  indexfi  9400  fsuppsssupp  9421  marypha1lem  9473  marypha2  9479  supmo  9492  infmo  9535  oieu  9579  brwdom2  9613  ixpiunwdom  9630  cantnfval2  9709  cantnfle  9711  cantnflt  9712  cantnf  9733  wemapwe  9737  cnfcom  9740  frrlem15  9797  rankonidlem  9868  r1pwcl  9887  eldju2ndl  9964  eldju2ndr  9965  djuun  9966  infxpenlem  10053  infxpenc2lem1  10059  fseqenlem1  10064  dfac8clem  10072  mappwen  10152  dfac3  10161  dfac5  10169  dfac12lem3  10186  infunsdom  10253  coftr  10313  ssfin4  10350  domfin4  10351  fin23lem26  10365  fin23lem22  10367  fin23lem28  10380  fin23lem32  10384  fin23lem40  10391  isf32lem5  10397  compssiso  10414  isf34lem4  10417  isfin1-3  10426  fin1a2lem13  10452  hsmexlem2  10467  hsmexlem4  10469  zorn2lem1  10536  ttukeylem6  10554  iundom2g  10580  konigthlem  10608  pwcfsdom  10623  fpwwe2lem11  10681  fpwwe2  10683  pwfseqlem3  10700  winalim2  10736  r1wunlim  10777  inttsk  10814  inar1  10815  grur1  10860  nqereq  10975  ltexprlem7  11082  prlem936  11087  00id  11436  addlid  11444  ltord1  11789  divdiv1  11978  divdiv2  11979  conjmul  11984  ltdivmul  12143  ledivmul  12144  lt2mul2div  12146  ltdiv23  12159  lediv23  12160  lediv12a  12161  ledivp1  12170  negfi  12217  nn0nndivcl  12598  nn0ge0div  12687  peano2uz2  12706  peano5uzi  12707  eluzp1m1  12904  qbtwnre  13241  xralrple  13247  xleadd1a  13295  xmulge0  13326  xmulass  13329  xlemul1a  13330  iooshf  13466  divelunit  13534  eluzgtdifelfzo  13766  modadd1  13948  modmul1  13965  seqcl2  14061  seqfveq2  14065  seqid2  14089  seqhomo  14090  seqdistr  14094  mulexpz  14143  leexp2r  14214  expnlbnd2  14273  expmulnbnd  14274  hashmap  14474  hashfun  14476  hashbclem  14491  hashfacen  14493  hashf1lem2  14495  hashf1  14496  ccatsymb  14620  swrdwrdsymb  14700  swrdsb0eq  14701  ccatpfx  14739  swrdswrd  14743  wrdind  14760  wrd2ind  14761  swrdccatin1  14763  swrdccatin2  14767  pfxccatin12lem2  14769  pfxccatin12  14771  swrdccat  14773  repswswrd  14822  0csh0  14831  cshwidxmod  14841  2cshw  14851  cshweqrep  14859  relexp0g  15061  relexpsucnnr  15064  relexpindlem  15102  01sqrexlem1  15281  01sqrexlem6  15286  rlim  15531  rlimclim1  15581  climsup  15706  caurcvg2  15714  caucvgb  15716  iseralt  15721  sumss  15760  fsum2dlem  15806  mptfzshft  15814  modfsummod  15830  o1fsum  15849  incexclem  15872  divrcnv  15888  flo1  15890  fprodrev  16013  fprod2dlem  16016  ruclem6  16271  moddvds  16301  dvdsaddre2b  16344  dvdsflip  16354  addmodlteqALT  16362  nn0o  16420  fldivndvdslt  16453  bitsf1ocnv  16481  bitsf1  16483  sadcaddlem  16494  bezoutlem2  16577  bezoutlem4  16579  lcmgcdlem  16643  prmind2  16722  isprm5  16744  isprm6  16751  prmdvdsncoprmbd  16764  cncongrprm  16766  hashdvds  16812  crth  16815  eulerthlem2  16819  prmdiveq  16823  hashgcdlem  16825  hashgcdeq  16827  iserodd  16873  pclem  16876  pcprendvds2  16879  pcexp  16897  pcneg  16912  pc2dvds  16917  pcmpt  16930  prmpwdvds  16942  pockthg  16944  prmreclem5  16958  4sqlem11  16993  ramub2  17052  ramubcl  17056  ram0  17060  ramub1lem2  17065  ramcl  17067  prmgaplem3  17091  prmgaplem6  17094  setscom  17217  sscpwex  17859  initoeu2  18061  setcinv  18135  funcestrcsetclem9  18193  funcsetcestrclem9  18208  fullsetcestrc  18211  1stfcl  18242  2ndfcl  18243  hofpropd  18312  isacs3lem  18587  isacs4lem  18589  acsmap2d  18600  subsubmgm  18723  submnd0  18776  mndpsuppss  18778  subsubm  18829  insubm  18831  frmdup1  18877  frmdup3lem  18879  sgrp2nmndlem2  18937  isgrpinv  19011  subsubg  19167  cycsubgcl  19224  conjghm  19267  qusghm  19273  gsumwrev  19385  gsmsymgrfixlem1  19445  symgfixelsi  19453  symgsssg  19485  symgfisg  19486  psgnunilem2  19513  odf1o2  19591  sylow1lem1  19616  odcau  19622  pgpfi  19623  pgpssslw  19632  fislw  19643  efgtlen  19744  efginvrel2  19745  efgrelexlemb  19768  efgredeu  19770  efgcpbllemb  19773  frgpup1  19793  lt6abl  19913  gsum2d  19990  gsum2d2lem  19991  gsum2d2  19992  telgsumfzslem  20006  dmdprdsplit2lem  20065  ablfacrp  20086  pgpfac1lem3  20097  gsummgp0  20315  irredrmul  20427  subsubrng  20563  subsubrg  20598  rngcinv  20637  ringcinv  20671  fldhmsubc  20786  islss4  20960  lspextmo  21055  lspsnat  21147  prmirredlem  21483  znf1o  21570  znidomb  21580  frgpcyg  21592  psgnghm  21598  psgndiflemB  21618  frlmlbs  21817  frlmup1  21818  lindfind  21836  islindf3  21846  lindfmm  21847  issubassa3  21886  resspsradd  21995  resspsrmul  21996  psdmul  22170  coe1tmmul2  22279  pf1ind  22359  mamulid  22447  mat1dimelbas  22477  mdetdiaglem  22604  mdetralt2  22615  mndifsplit  22642  smadiadetglem2  22678  1elcpmat  22721  pmatcollpw3lem  22789  chfacfisf  22860  chfacfisfcpmat  22861  chfacffsupp  22862  chfacfscmulfsupp  22865  chfacfscmulgsum  22866  chfacfpmmulfsupp  22869  chfacfpmmulgsum  22870  chfacfpmmulgsum2  22871  cayhamlem1  22872  cpmadugsumlemF  22882  cayleyhamilton1  22898  tgcl  22976  pptbas  23015  clsval2  23058  mretopd  23100  lmbr2  23267  cncls2  23281  nrmsep  23365  regsep2  23384  cmpsublem  23407  cmpsub  23408  tgcmp  23409  uncmp  23411  hauscmplem  23414  iunconnlem  23435  1stcrest  23461  2ndcctbss  23463  2ndcsep  23467  dis2ndc  23468  hausllycmp  23502  dislly  23505  kgentopon  23546  1stckgen  23562  kgencn3  23566  ptpjpre1  23579  ptbasin  23585  ptpjopn  23620  dfac14  23626  ptcnplem  23629  txcn  23634  txindis  23642  txdis1cn  23643  ptrescn  23647  txcmplem1  23649  txcmp  23651  txhaus  23655  txlm  23656  tx1stc  23658  txkgen  23660  xkococn  23668  qtopcn  23722  kqreglem1  23749  kqreglem2  23750  kqnrmlem1  23751  kqnrmlem2  23752  hmeoimaf1o  23778  reghmph  23801  nrmhmph  23802  txhmeo  23811  ptuncnv  23815  filconn  23891  fbasrn  23892  fmfnfmlem2  23963  flimfnfcls  24036  cnpfcfi  24048  alexsublem  24052  alexsubALTlem2  24056  alexsubALTlem3  24057  alexsubALTlem4  24058  alexsubALT  24059  ptcmplem3  24062  cnextfval  24070  tsmsxp  24163  imasdsf1olem  24383  bl2in  24410  blssps  24434  blss  24435  blssexps  24436  blssex  24437  blcld  24518  stdbdxmet  24528  met1stc  24534  prdsxmslem2  24542  metcnp3  24553  metcnpi3  24559  txmetcnp  24560  nmo0  24756  nmoid  24763  icccmplem1  24844  icccmp  24847  xrge0tsms  24856  metdseq0  24876  cnheiborlem  24986  cnheibor  24987  cnllycmp  24988  pcoval2  25049  cmetcaulem  25322  iscmet3lem1  25325  iscmet3lem2  25326  equivcau  25334  lmcau  25347  cncmet  25356  ivthlem2  25487  ivthlem3  25488  ovoliunlem2  25538  ovolscalem2  25549  uniioombl  25624  dyaddisj  25631  opnmbllem  25636  volivth  25642  ismbfd  25674  ismbf3d  25689  mbfimaopnlem  25690  mbfinf  25700  itg1addlem4  25734  mbfi1fseqlem1  25750  mbfi1fseqlem3  25752  mbfi1fseqlem4  25753  mbfi1fseqlem5  25754  mbfi1fseqlem6  25755  itg2seq  25777  itg2lea  25779  itg2split  25784  itg2cnlem1  25796  bddiblnc  25877  limciun  25929  dvmptfsum  26013  rolle  26028  c1lip1  26036  dvcnvrelem1  26056  dvcnvre  26058  dvcvx  26059  itgsubst  26090  tdeglem4  26099  mdegmullem  26117  plyco0  26231  coemullem  26289  dgreq0  26305  dgrmul  26310  dgrco  26315  elqaalem2  26362  aannenlem1  26370  aaliou3lem9  26392  ulmres  26431  ulmshftlem  26432  angneg  26846  dcubic  26889  cxploglim  27021  cxploglim2  27022  scvxcvx  27029  lgamgulmlem5  27076  lgamcvg2  27098  ftalem2  27117  basellem3  27126  basellem4  27127  sqff1o  27225  fsumdvdsdiaglem  27226  dvdsflsumcom  27231  mpodvdsmulf1o  27237  dvdsmulf1o  27239  fsumvma2  27258  logfac2  27261  logfacrlim  27268  logexprlim  27269  dchrelbasd  27283  lgsne0  27379  lgsqrlem2  27391  lgsqrmodndvds  27397  gausslemma2dlem1a  27409  lgseisenlem2  27420  lgsquadlem1  27424  lgsquadlem2  27425  lgsquadlem3  27426  lgsquad2lem2  27429  2sqlem8  27470  2sqlem11  27473  2sqreultlem  27491  2sqreunnltlem  27494  chpo1ubb  27525  vmadivsum  27526  rplogsumlem2  27529  rpvmasumlem  27531  dchrmusum2  27538  dchrvmasumlem1  27539  dchrisum0fno1  27555  dchrisum0re  27557  dchrisum0lem1  27560  dchrisum0lem2  27562  dchrisum0lem3  27563  dchrisum0  27564  mulogsumlem  27575  mulog2sumlem2  27579  vmalogdivsum2  27582  logsqvma  27586  log2sumbnd  27588  selberglem3  27591  selberg  27592  selberg2lem  27594  selberg2b  27596  selberg3lem2  27602  pntrmax  27608  pntrsumo1  27609  pntlemn  27644  pntlemp  27654  qabvle  27669  ostthlem1  27671  ostthlem2  27672  ostth2lem2  27678  ostth3  27682  sltres  27707  nosupno  27748  nosupbnd2  27761  noinfno  27763  noinfbnd2  27776  etasslt  27858  cuteq1  27878  addsproplem2  28003  mulsval  28135  precsexlem11  28241  zmulscld  28383  idmot  28545  brbtwn2  28920  colinearalglem4  28924  colinearalg  28925  ax5seglem9  28952  axpaschlem  28955  axcontlem2  28980  axcontlem7  28985  axcontlem8  28986  eengtrkg  29001  upgr1eopALT  29134  uspgredg2vlem  29240  subumgr  29305  nbgr0edglem  29373  edgnbusgreu  29384  nb3grprlem1  29397  wlkl1loop  29656  pthdivtx  29747  usgr2pth  29784  crctcshwlkn0  29841  wlklnwwlkln1  29888  wwlksnext  29913  clwwlkccatlem  30008  clwlkclwwlklem2a  30017  clwwlkinwwlk  30059  clwwlkn1loopb  30062  clwwlkf  30066  wwlksext2clwwlk  30076  wwlksubclwwlk  30077  clwwlknscsh  30081  clwwlknon1  30116  clwwlknonex2e  30129  1conngr  30213  n4cyclfrgr  30310  numclwwlk2lem1lem  30361  2clwwlk2clwwlk  30369  numclwwlk1lem2f1  30376  numclwlk1lem1  30388  numclwwlk2lem1  30395  numclwlk2lem2f  30396  numclwwlk7  30410  frgrogt3nreg  30416  grpoidinvlem1  30523  grpoidinvlem3  30525  grporcan  30537  nmlnoubi  30815  blocnilem  30823  ipblnfi  30874  htthlem  30936  ocsh  31302  shmodsi  31408  pjhthlem2  31411  5oalem2  31674  eigposi  31855  nmopub2tALT  31928  nmfnleub2  31945  nmcexi  32045  nmopcoi  32114  kbass3  32137  mdslmd1lem1  32344  mdslmd1lem2  32345  chirredlem2  32410  chirredlem4  32412  mdsymlem3  32424  mdsymlem5  32426  sumdmdii  32434  sumdmdlem  32437  sumdmdlem2  32438  foresf1o  32523  disjxpin  32601  1stpreimas  32715  resf1o  32741  nn0xmulclb  32775  wrdt2ind  32938  xrge0tsmsd  33065  gsumvsca1  33232  gsumvsca2  33233  islinds5  33395  1arithidomlem2  33564  irngnzply1  33741  mdetpmtr1  33822  mdetpmtr2  33823  pstmxmet  33896  qqhghm  33989  qqhrhm  33990  esumpcvgval  34079  volmeas  34232  imambfm  34264  dya2iocnrect  34283  oddpwdc  34356  sseqf  34394  orvcgteel  34470  orvclteel  34475  ballotlemsf1o  34516  bnj1110  34996  bnj1118  34998  f1resveqaeq  35099  txpconn  35237  connpconn  35240  cnllysconn  35250  rellysconn  35256  cvmsss2  35279  cvmlift2lem9  35316  satf00  35379  fmlasuc  35391  mrsubfval  35513  mppsval  35577  dfon2lem6  35789  wzel  35825  ifscgr  36045  cgrxfr  36056  btwnconn1lem5  36092  btwnconn1lem6  36093  btwnconn1lem12  36099  brsegle  36109  finminlem  36319  nn0prpwlem  36323  fnessref  36358  refssfne  36359  neibastop1  36360  topjoin  36366  fnemeet2  36368  weiunse  36469  bj-prmoore  37116  bj-finsumval0  37286  topdifinffinlem  37348  lindsadd  37620  matunitlindflem2  37624  poimirlem28  37655  poimirlem32  37659  opnmbllem0  37663  mblfinlem1  37664  mblfinlem4  37667  ismblfin  37668  mbfresfi  37673  itg2addnclem  37678  itg2addnclem3  37680  itg2addnc  37681  unirep  37721  frinfm  37742  sdclem2  37749  geomcau  37766  istotbnd3  37778  sstotbnd2  37781  sstotbnd  37782  sstotbnd3  37783  totbndbnd  37796  cntotbnd  37803  ismtyres  37815  heibor1lem  37816  heiborlem1  37818  heiborlem8  37825  ismndo1  37880  isdivrngo  37957  unichnidl  38038  erimeq2  38679  cvlcvr1  39340  ishlat3N  39355  llnmlplnN  39541  islvol2aN  39594  4atlem4c  39603  4atlem4d  39604  isline2  39776  isline3  39778  linepsubclN  39953  lhpexle3lem  40013  lhpjat2  40023  cdlemd4  40203  cdleme0cq  40217  cdleme32fva  40439  cdleme32fvaw  40441  tendo0mul  40828  tendo0mulr  40829  diameetN  41058  dvhvaddcl  41097  dvhvaddcomN  41098  cdlemm10N  41120  dvadiaN  41130  djavalN  41137  dihvalcqat  41241  dihopelvalcpre  41250  djhval  41400  dihjat1lem  41430  sticksstones11  42157  sticksstones22  42169  metakunt15  42220  metakunt16  42221  f1o2d2  42274  remul01  42437  zaddcom  42482  zmulcom  42486  fidomncyc  42545  evlselvlem  42596  evlselv  42597  fsuppind  42600  mhpind  42604  prjspertr  42615  prjsprellsp  42621  elrfi  42705  nacsfix  42723  fzsplit1nn0  42765  eldioph2  42773  lzenom  42781  irrapxlem3  42835  pellexlem5  42844  pell1234qrne0  42864  pell1234qrmulcl  42866  pell14qrdich  42880  pell1qrge1  42881  pellqrex  42890  reglogltb  42902  reglogleb  42903  rmxypairf1o  42923  rmxycomplete  42929  monotoddzzfi  42954  congadd  42978  congsym  42980  acongrep  42992  jm2.19lem3  43003  jm2.19lem4  43004  jm2.22  43007  jm2.25  43011  expdiophlem1  43033  wepwsolem  43054  kelac1  43075  lmhmfgsplit  43098  pwslnm  43106  hbtlem6  43141  hbt  43142  mon1psubm  43211  deg1mhm  43212  omord2lim  43313  succlg  43341  onmcl  43344  ofoafo  43369  ofoacom  43374  fzunt  43468  fzuntd  43469  fzunt1d  43470  fzuntgd  43471  iunrelexp0  43715  dssmapnvod  44033  gsumws3  44209  gsumws4  44210  mulltgt0  45027  fnchoice  45034  disjrnmpt2  45193  fzisoeu  45312  fsumiunss  45590  climinf  45621  mullimc  45631  mullimcf  45638  stoweidlem14  46029  stoweidlem17  46032  stoweidlem34  46049  stoweidlem50  46065  fourierdlem42  46164  fourierdlem62  46183  fourierdlem71  46192  fourierdlem76  46197  qndenserrnbllem  46309  subsaliuncl  46373  sge0resplit  46421  upwrdfi  46902  3f1oss1  47087  2reu8i  47125  addmodne  47346  fundcmpsurinjpreimafv  47395  iccpartigtl  47410  prproropf1olem2  47491  prproropf1olem4  47493  paireqne  47498  prmdvdsfmtnof1lem2  47572  bgoldbtbndlem3  47794  bgoldbtbnd  47796  uspgrimprop  47873  grimcnv  47879  gricushgr  47886  grimedg  47903  grtrimap  47915  isubgr3stgrlem6  47938  isubgr3stgrlem7  47939  isubgr3stgrlem8  47940  isubgr3stgrlem9  47941  grlimfn  47946  gpg5nbgrvtx03starlem2  48025  gpg5nbgrvtx13starlem2  48028  uspgrsprf1  48063  isassintop  48126  2zlidl  48156  2zrngnmrid  48172  rngcinvALTV  48192  funcringcsetcALTV2lem9  48214  ringcinvALTV  48226  funcringcsetclem9ALTV  48237  fldhmsubcALTV  48249  gsumlsscl  48296  lincsum  48346  lindslinindsimp1  48374  lindslinindimp2lem4  48378  lincresunitlem2  48393  elfzolborelfzop1  48436  elbigo2  48473  digexp  48528  dig1  48529  nn0sumshdiglemB  48541  1arymaptf1  48563  2arymaptf1  48574  itcoval1  48584  itcoval2  48585  itcoval3  48586  itcovalsucov  48589  ackvalsuc1mpt  48599  itschlc0xyqsol  48688  brab2dd  48741  thincciso  49102  indthinc  49109  indthincALT  49110  oduoppcciso  49170