Theorem ad2antrl 726

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  simprl  769  simprll  777  simprlr  778  simprl1  1218  simprl2  1219  simprl3  1220  disjxiun  5093  reusv2lem4  5348  axprlem5  5374  fr2nr  5602  somin1  6077  tz7.7  6332  f1oprg  6816  soisores  7258  elovmporab1w  7582  elovmporab1  7583  sorpssi  7648  onint  7707  ordsucelsuc  7739  elxp5  7842  wemoiso  7888  wemoiso2  7889  el2xptp0  7950  ressuppss  8073  fprlem1  8190  tz7.48lem  8346  oalimcl  8466  oeeui  8508  oaabs2  8554  omabs  8556  swoer  8603  ralxpmap  8759  pw2f1olem  8945  enfixsn  8950  mapxpen  9012  mapunen  9015  php  9079  unxpdomlem2  9120  unxpdomlem3  9121  findcard3OLD  9155  isfinite2  9170  domunfican  9189  fodomfi  9194  fissuni  9226  fipreima  9227  indexfi  9229  fsuppsssupp  9246  marypha1lem  9294  marypha2  9300  supmo  9313  infmo  9356  oieu  9400  brwdom2  9434  ixpiunwdom  9451  cantnfval2  9530  cantnfle  9532  cantnflt  9533  cantnf  9554  wemapwe  9558  cnfcom  9561  frrlem15  9618  rankonidlem  9689  r1pwcl  9708  eldju2ndl  9785  eldju2ndr  9786  djuun  9787  infxpenlem  9874  infxpenc2lem1  9880  fseqenlem1  9885  dfac8clem  9893  mappwen  9973  dfac3  9982  dfac5  9989  dfac12lem3  10006  infunsdom  10075  coftr  10134  ssfin4  10171  domfin4  10172  fin23lem26  10186  fin23lem22  10188  fin23lem28  10201  fin23lem32  10205  fin23lem40  10212  isf32lem5  10218  compssiso  10235  isf34lem4  10238  isfin1-3  10247  fin1a2lem13  10273  hsmexlem2  10288  hsmexlem4  10290  zorn2lem1  10357  ttukeylem6  10375  iundom2g  10401  konigthlem  10429  pwcfsdom  10444  fpwwe2lem11  10502  fpwwe2  10504  pwfseqlem3  10521  winalim2  10557  r1wunlim  10598  inttsk  10635  inar1  10636  grur1  10681  nqereq  10796  ltexprlem7  10903  prlem936  10908  00id  11255  addid2  11263  ltord1  11606  divdiv1  11791  divdiv2  11792  conjmul  11797  ltdivmul  11955  ledivmul  11956  lt2mul2div  11958  ltdiv23  11971  lediv23  11972  lediv12a  11973  ledivp1  11982  negfi  12029  nn0nndivcl  12409  nn0ge0div  12494  peano2uz2  12513  peano5uzi  12514  eluzp1m1  12713  qbtwnre  13038  xralrple  13044  xleadd1a  13092  xmulge0  13123  xmulass  13126  xlemul1a  13127  iooshf  13263  divelunit  13331  eluzgtdifelfzo  13554  modadd1  13733  modmul1  13749  seqcl2  13846  seqfveq2  13850  seqid2  13874  seqhomo  13875  seqdistr  13879  mulexpz  13928  leexp2r  13997  expnlbnd2  14054  expmulnbnd  14055  hashmap  14254  hashfun  14256  hashbclem  14268  hashfacen  14270  hashfacenOLD  14271  hashf1lem2  14274  hashf1  14275  ccatsymb  14389  swrdwrdsymb  14473  swrdsb0eq  14474  ccatpfx  14512  swrdswrd  14516  wrdind  14533  wrd2ind  14534  swrdccatin1  14536  swrdccatin2  14540  pfxccatin12lem2  14542  pfxccatin12  14544  swrdccat  14546  repswswrd  14595  0csh0  14604  cshwidxmod  14614  2cshw  14624  cshweqrep  14632  relexp0g  14832  relexpsucnnr  14835  relexpindlem  14873  sqrlem1  15053  sqrlem6  15058  rlim  15303  rlimclim1  15353  climsup  15480  caurcvg2  15488  caucvgb  15490  iseralt  15495  sumss  15535  fsum2dlem  15581  mptfzshft  15589  modfsummod  15605  o1fsum  15624  incexclem  15647  divrcnv  15663  flo1  15665  fprodrev  15786  fprod2dlem  15789  ruclem6  16043  moddvds  16073  dvdsaddre2b  16115  dvdsflip  16125  addmodlteqALT  16133  nn0o  16191  fldivndvdslt  16222  bitsf1ocnv  16250  bitsf1  16252  sadcaddlem  16263  bezoutlem2  16347  bezoutlem4  16349  lcmgcdlem  16408  prmind2  16487  isprm5  16509  isprm6  16516  prmdvdsncoprmbd  16528  cncongrprm  16530  hashdvds  16573  crth  16576  eulerthlem2  16580  prmdiveq  16584  hashgcdlem  16586  hashgcdeq  16587  iserodd  16633  pclem  16636  pcprendvds2  16639  pcexp  16657  pcneg  16672  pc2dvds  16677  pcmpt  16690  prmpwdvds  16702  pockthg  16704  prmreclem5  16718  4sqlem11  16753  ramub2  16812  ramubcl  16816  ram0  16820  ramub1lem2  16825  ramcl  16827  prmgaplem3  16851  prmgaplem6  16854  setscom  16978  sscpwex  17624  initoeu2  17828  setcinv  17902  funcestrcsetclem9  17962  funcsetcestrclem9  17977  fullsetcestrc  17980  1stfcl  18011  2ndfcl  18012  hofpropd  18082  isacs3lem  18357  isacs4lem  18359  acsmap2d  18370  submnd0  18511  subsubm  18552  insubm  18554  frmdup1  18599  frmdup3lem  18601  sgrp2nmndlem2  18659  isgrpinv  18728  subsubg  18874  cycsubgcl  18921  conjghm  18961  qusghm  18967  gsumwrev  19069  gsmsymgrfixlem1  19131  symgfixelsi  19139  symgsssg  19171  symgfisg  19172  psgnunilem2  19199  odf1o2  19274  sylow1lem1  19299  odcau  19305  pgpfi  19306  pgpssslw  19315  fislw  19326  efgtlen  19427  efginvrel2  19428  efgrelexlemb  19451  efgredeu  19453  efgcpbllemb  19456  frgpup1  19476  lt6abl  19590  gsum2d  19667  gsum2d2lem  19668  gsum2d2  19669  telgsumfzslem  19683  dmdprdsplit2lem  19742  ablfacrp  19763  pgpfac1lem3  19774  gsummgp0  19941  irredrmul  20043  subsubrg  20154  islss4  20329  lspextmo  20423  lspsnat  20512  prmirredlem  20799  znf1o  20864  znidomb  20874  frgpcyg  20886  psgnghm  20890  psgndiflemB  20910  frlmlbs  21109  frlmup1  21110  lindfind  21128  islindf3  21138  lindfmm  21139  issubassa3  21177  resspsradd  21290  resspsrmul  21291  coe1tmmul2  21552  pf1ind  21626  mamulid  21695  mat1dimelbas  21725  mdetdiaglem  21852  mdetralt2  21863  mndifsplit  21890  smadiadetglem2  21926  1elcpmat  21969  pmatcollpw3lem  22037  chfacfisf  22108  chfacfisfcpmat  22109  chfacffsupp  22110  chfacfscmulfsupp  22113  chfacfscmulgsum  22114  chfacfpmmulfsupp  22117  chfacfpmmulgsum  22118  chfacfpmmulgsum2  22119  cayhamlem1  22120  cpmadugsumlemF  22130  cayleyhamilton1  22146  tgcl  22224  pptbas  22263  clsval2  22306  mretopd  22348  lmbr2  22515  cncls2  22529  nrmsep  22613  regsep2  22632  cmpsublem  22655  cmpsub  22656  tgcmp  22657  uncmp  22659  hauscmplem  22662  iunconnlem  22683  1stcrest  22709  2ndcctbss  22711  2ndcsep  22715  dis2ndc  22716  hausllycmp  22750  dislly  22753  kgentopon  22794  1stckgen  22810  kgencn3  22814  ptpjpre1  22827  ptbasin  22833  ptpjopn  22868  dfac14  22874  ptcnplem  22877  txcn  22882  txindis  22890  txdis1cn  22891  ptrescn  22895  txcmplem1  22897  txcmp  22899  txhaus  22903  txlm  22904  tx1stc  22906  txkgen  22908  xkococn  22916  qtopcn  22970  kqreglem1  22997  kqreglem2  22998  kqnrmlem1  22999  kqnrmlem2  23000  hmeoimaf1o  23026  reghmph  23049  nrmhmph  23050  txhmeo  23059  ptuncnv  23063  filconn  23139  fbasrn  23140  fmfnfmlem2  23211  flimfnfcls  23284  cnpfcfi  23296  alexsublem  23300  alexsubALTlem2  23304  alexsubALTlem3  23305  alexsubALTlem4  23306  alexsubALT  23307  ptcmplem3  23310  cnextfval  23318  tsmsxp  23411  imasdsf1olem  23631  bl2in  23658  blssps  23682  blss  23683  blssexps  23684  blssex  23685  blcld  23766  stdbdxmet  23776  met1stc  23782  prdsxmslem2  23790  metcnp3  23801  metcnpi3  23807  txmetcnp  23808  nmo0  24004  nmoid  24011  icccmplem1  24090  icccmp  24093  xrge0tsms  24102  metdseq0  24122  cnheiborlem  24222  cnheibor  24223  cnllycmp  24224  pcoval2  24284  cmetcaulem  24557  iscmet3lem1  24560  iscmet3lem2  24561  equivcau  24569  lmcau  24582  cncmet  24591  ivthlem2  24721  ivthlem3  24722  ovoliunlem2  24772  ovolscalem2  24783  uniioombl  24858  dyaddisj  24865  opnmbllem  24870  volivth  24876  ismbfd  24908  ismbf3d  24923  mbfimaopnlem  24924  mbfinf  24934  itg1addlem4  24968  itg1addlem4OLD  24969  mbfi1fseqlem1  24985  mbfi1fseqlem3  24987  mbfi1fseqlem4  24988  mbfi1fseqlem5  24989  mbfi1fseqlem6  24990  itg2seq  25012  itg2lea  25014  itg2split  25019  itg2cnlem1  25031  bddiblnc  25111  limciun  25163  dvmptfsum  25244  rolle  25259  c1lip1  25266  dvcnvrelem1  25286  dvcnvre  25288  dvcvx  25289  itgsubst  25318  tdeglem4  25329  tdeglem4OLD  25330  mdegmullem  25348  plyco0  25458  coemullem  25516  dgreq0  25531  dgrmul  25536  dgrco  25541  elqaalem2  25585  aannenlem1  25593  aaliou3lem9  25615  ulmres  25652  ulmshftlem  25653  angneg  26058  dcubic  26101  cxploglim  26232  cxploglim2  26233  scvxcvx  26240  lgamgulmlem5  26287  lgamcvg2  26309  ftalem2  26328  basellem3  26337  basellem4  26338  sqff1o  26436  fsumdvdsdiaglem  26437  dvdsflsumcom  26442  dvdsmulf1o  26448  fsumvma2  26467  logfac2  26470  logfacrlim  26477  logexprlim  26478  dchrelbasd  26492  lgsne0  26588  lgsqrlem2  26600  lgsqrmodndvds  26606  gausslemma2dlem1a  26618  lgseisenlem2  26629  lgsquadlem1  26633  lgsquadlem2  26634  lgsquadlem3  26635  lgsquad2lem2  26638  2sqlem8  26679  2sqlem11  26682  2sqreultlem  26700  2sqreunnltlem  26703  chpo1ubb  26734  vmadivsum  26735  rplogsumlem2  26738  rpvmasumlem  26740  dchrmusum2  26747  dchrvmasumlem1  26748  dchrisum0fno1  26764  dchrisum0re  26766  dchrisum0lem1  26769  dchrisum0lem2  26771  dchrisum0lem3  26772  dchrisum0  26773  mulogsumlem  26784  mulog2sumlem2  26788  vmalogdivsum2  26791  logsqvma  26795  log2sumbnd  26797  selberglem3  26800  selberg  26801  selberg2lem  26803  selberg2b  26805  selberg3lem2  26811  pntrmax  26817  pntrsumo1  26818  pntlemn  26853  pntlemp  26863  qabvle  26878  ostthlem1  26880  ostthlem2  26881  ostth2lem2  26887  ostth3  26891  sltres  26915  nosupno  26956  nosupbnd2  26969  noinfno  26971  noinfbnd2  26984  etasslt  27057  idmot  27186  brbtwn2  27561  colinearalglem4  27565  colinearalg  27566  ax5seglem9  27593  axpaschlem  27596  axcontlem2  27621  axcontlem7  27626  axcontlem8  27627  eengtrkg  27642  upgr1eopALT  27775  uspgredg2vlem  27878  subumgr  27943  nbgr0vtxlem  28010  edgnbusgreu  28022  nb3grprlem1  28035  wlkl1loop  28293  pthdivtx  28384  usgr2pth  28419  crctcshwlkn0  28473  wlklnwwlkln1  28520  wwlksnext  28545  clwwlkccatlem  28640  clwlkclwwlklem2a  28649  clwwlkinwwlk  28691  clwwlkn1loopb  28694  clwwlkf  28698  wwlksext2clwwlk  28708  wwlksubclwwlk  28709  clwwlknscsh  28713  clwwlknon1  28748  clwwlknonex2e  28761  1conngr  28845  n4cyclfrgr  28942  numclwwlk2lem1lem  28993  2clwwlk2clwwlk  29001  numclwwlk1lem2f1  29008  numclwlk1lem1  29020  numclwwlk2lem1  29027  numclwlk2lem2f  29028  numclwwlk7  29042  frgrogt3nreg  29048  grpoidinvlem1  29153  grpoidinvlem3  29155  grporcan  29167  nmlnoubi  29445  blocnilem  29453  ipblnfi  29504  htthlem  29566  ocsh  29932  shmodsi  30038  pjhthlem2  30041  5oalem2  30304  eigposi  30485  nmopub2tALT  30558  nmfnleub2  30575  nmcexi  30675  nmopcoi  30744  kbass3  30767  mdslmd1lem1  30974  mdslmd1lem2  30975  chirredlem2  31040  chirredlem4  31042  mdsymlem3  31054  mdsymlem5  31056  sumdmdii  31064  sumdmdlem  31067  sumdmdlem2  31068  foresf1o  31137  disjxpin  31212  1stpreimas  31323  resf1o  31350  nn0xmulclb  31379  wrdt2ind  31510  xrge0tsmsd  31602  gsumvsca1  31764  gsumvsca2  31765  islinds5  31858  mdetpmtr1  32069  mdetpmtr2  32070  pstmxmet  32143  qqhghm  32234  qqhrhm  32235  esumpcvgval  32342  volmeas  32495  imambfm  32527  dya2iocnrect  32546  oddpwdc  32619  sseqf  32657  orvcgteel  32732  orvclteel  32737  ballotlemsf1o  32778  bnj1110  33259  bnj1118  33261  f1resveqaeq  33354  txpconn  33491  connpconn  33494  cnllysconn  33504  rellysconn  33510  cvmsss2  33533  cvmlift2lem9  33570  satf00  33633  fmlasuc  33645  mrsubfval  33767  mppsval  33831  dfon2lem6  34047  frxp2  34073  poxp3  34078  frxp3  34079  wzel  34097  addsproplem2  34234  ifscgr  34483  cgrxfr  34494  btwnconn1lem5  34530  btwnconn1lem6  34531  btwnconn1lem12  34537  brsegle  34547  finminlem  34644  nn0prpwlem  34648  fnessref  34683  refssfne  34684  neibastop1  34685  topjoin  34691  fnemeet2  34693  bj-prmoore  35440  bj-finsumval0  35610  topdifinffinlem  35672  lindsadd  35926  matunitlindflem2  35930  poimirlem28  35961  poimirlem32  35965  opnmbllem0  35969  mblfinlem1  35970  mblfinlem4  35973  ismblfin  35974  mbfresfi  35979  itg2addnclem  35984  itg2addnclem3  35986  itg2addnc  35987  unirep  36027  frinfm  36049  sdclem2  36056  geomcau  36073  istotbnd3  36085  sstotbnd2  36088  sstotbnd  36089  sstotbnd3  36090  totbndbnd  36103  cntotbnd  36110  ismtyres  36122  heibor1lem  36123  heiborlem1  36125  heiborlem8  36132  ismndo1  36187  isdivrngo  36264  unichnidl  36345  erimeq2  36996  cvlcvr1  37657  ishlat3N  37672  llnmlplnN  37858  islvol2aN  37911  4atlem4c  37920  4atlem4d  37921  isline2  38093  isline3  38095  linepsubclN  38270  lhpexle3lem  38330  lhpjat2  38340  cdlemd4  38520  cdleme0cq  38534  cdleme32fva  38756  cdleme32fvaw  38758  tendo0mul  39145  tendo0mulr  39146  diameetN  39375  dvhvaddcl  39414  dvhvaddcomN  39415  cdlemm10N  39437  dvadiaN  39447  djavalN  39454  dihvalcqat  39558  dihopelvalcpre  39567  djhval  39717  dihjat1lem  39747  sticksstones11  40420  sticksstones22  40432  metakunt15  40447  metakunt16  40448  evlsbagval  40586  fsuppind  40590  mhpind  40594  mhphf  40596  remul01  40701  prjspertr  40755  prjsprellsp  40761  elrfi  40829  nacsfix  40847  fzsplit1nn0  40889  eldioph2  40897  lzenom  40905  irrapxlem3  40959  pellexlem5  40968  pell1234qrne0  40988  pell1234qrmulcl  40990  pell14qrdich  41004  pell1qrge1  41005  pellqrex  41014  reglogltb  41026  reglogleb  41027  rmxypairf1o  41047  rmxycomplete  41053  monotoddzzfi  41078  congadd  41102  congsym  41104  acongrep  41116  jm2.19lem3  41127  jm2.19lem4  41128  jm2.22  41131  jm2.25  41135  expdiophlem1  41157  wepwsolem  41181  kelac1  41202  lmhmfgsplit  41225  pwslnm  41233  hbtlem6  41268  hbt  41269  mon1psubm  41345  deg1mhm  41346  succlg  41366  ofoafo  41374  ofoacom  41379  fzunt  41436  fzuntd  41437  fzunt1d  41438  fzuntgd  41439  iunrelexp0  41683  dssmapnvod  42001  gsumws3  42180  gsumws4  42181  mulltgt0  42938  fnchoice  42945  disjrnmpt2  43105  fzisoeu  43226  fsumiunss  43504  climinf  43535  mullimc  43545  mullimcf  43552  stoweidlem14  43943  stoweidlem17  43946  stoweidlem34  43963  stoweidlem50  43979  fourierdlem42  44078  fourierdlem62  44097  fourierdlem71  44106  fourierdlem76  44111  qndenserrnbllem  44223  subsaliuncl  44285  sge0resplit  44333  upwrdfi  44804  2reu8i  45023  fundcmpsurinjpreimafv  45278  iccpartigtl  45293  prproropf1olem2  45374  prproropf1olem4  45376  paireqne  45381  prmdvdsfmtnof1lem2  45455  bgoldbtbndlem3  45677  bgoldbtbnd  45679  isomushgr  45696  isomuspgrlem2c  45700  uspgrsprf1  45727  subsubmgm  45769  isassintop  45822  2zlidl  45910  2zrngnmrid  45926  rngcinv  45957  rngcinvALTV  45969  ringcinv  46008  funcringcsetcALTV2lem9  46020  ringcinvALTV  46032  funcringcsetclem9ALTV  46043  fldhmsubc  46060  fldhmsubcALTV  46078  mndpsuppss  46125  gsumlsscl  46137  lincsum  46188  lindslinindsimp1  46216  lindslinindimp2lem4  46220  lincresunitlem2  46235  elfzolborelfzop1  46278  elbigo2  46316  digexp  46371  dig1  46372  nn0sumshdiglemB  46384  1arymaptf1  46406  2arymaptf1  46417  itcoval1  46427  itcoval2  46428  itcoval3  46429  itcovalsucov  46432  ackvalsuc1mpt  46442  itschlc0xyqsol  46531  thincciso  46748  indthinc  46751  indthincALT  46752