Theorem ad2antrl 725

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

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  simprl  768  simprll  776  simprlr  777  simprl1  1217  simprl2  1218  simprl3  1219  disjxiun  5072  reusv2lem4  5325  axprlem5  5351  fr2nr  5568  somin1  6043  tz7.7  6296  f1oprg  6770  soisores  7207  elovmporab1w  7525  elovmporab1  7526  sorpssi  7591  onint  7649  ordsucelsuc  7678  elxp5  7779  wemoiso  7825  wemoiso2  7826  el2xptp0  7887  ressuppss  8008  fprlem1  8125  tz7.48lem  8281  oalimcl  8400  oeeui  8442  oaabs2  8488  omabs  8490  swoer  8537  ralxpmap  8693  pw2f1olem  8872  enfixsn  8877  mapxpen  8939  mapunen  8942  php  9002  unxpdomlem2  9037  unxpdomlem3  9038  findcard3  9066  isfinite2  9081  domunfican  9096  fodomfi  9101  fissuni  9133  fipreima  9134  indexfi  9136  fsuppsssupp  9153  marypha1lem  9201  marypha2  9207  supmo  9220  infmo  9263  oieu  9307  brwdom2  9341  ixpiunwdom  9358  cantnfval2  9436  cantnfle  9438  cantnflt  9439  cantnf  9460  wemapwe  9464  cnfcom  9467  frrlem15  9524  rankonidlem  9595  r1pwcl  9614  eldju2ndl  9691  eldju2ndr  9692  djuun  9693  infxpenlem  9778  infxpenc2lem1  9784  fseqenlem1  9789  dfac8clem  9797  mappwen  9877  dfac3  9886  dfac5  9893  dfac12lem3  9910  infunsdom  9979  coftr  10038  ssfin4  10075  domfin4  10076  fin23lem26  10090  fin23lem22  10092  fin23lem28  10105  fin23lem32  10109  fin23lem40  10116  isf32lem5  10122  compssiso  10139  isf34lem4  10142  isfin1-3  10151  fin1a2lem13  10177  hsmexlem2  10192  hsmexlem4  10194  zorn2lem1  10261  ttukeylem6  10279  iundom2g  10305  konigthlem  10333  pwcfsdom  10348  fpwwe2lem11  10406  fpwwe2  10408  pwfseqlem3  10425  winalim2  10461  r1wunlim  10502  inttsk  10539  inar1  10540  grur1  10585  nqereq  10700  ltexprlem7  10807  prlem936  10812  00id  11159  addid2  11167  ltord1  11510  divdiv1  11695  divdiv2  11696  conjmul  11701  ltdivmul  11859  ledivmul  11860  lt2mul2div  11862  ltdiv23  11875  lediv23  11876  lediv12a  11877  ledivp1  11886  negfi  11933  nn0nndivcl  12313  nn0ge0div  12398  peano2uz2  12417  peano5uzi  12418  eluzp1m1  12617  qbtwnre  12942  xralrple  12948  xleadd1a  12996  xmulge0  13027  xmulass  13030  xlemul1a  13031  iooshf  13167  divelunit  13235  eluzgtdifelfzo  13458  modadd1  13637  modmul1  13653  seqcl2  13750  seqfveq2  13754  seqid2  13778  seqhomo  13779  seqdistr  13783  mulexpz  13832  leexp2r  13901  expnlbnd2  13958  expmulnbnd  13959  hashmap  14159  hashfun  14161  hashbclem  14173  hashfacen  14175  hashfacenOLD  14176  hashf1lem2  14179  hashf1  14180  ccatsymb  14296  swrdwrdsymb  14384  swrdsb0eq  14385  ccatpfx  14423  swrdswrd  14427  wrdind  14444  wrd2ind  14445  swrdccatin1  14447  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12  14455  swrdccat  14457  repswswrd  14506  0csh0  14515  cshwidxmod  14525  2cshw  14535  cshweqrep  14543  relexp0g  14742  relexpsucnnr  14745  relexpindlem  14783  sqrlem1  14963  sqrlem6  14968  rlim  15213  rlimclim1  15263  climsup  15390  caurcvg2  15398  caucvgb  15400  iseralt  15405  sumss  15445  fsum2dlem  15491  mptfzshft  15499  modfsummod  15515  o1fsum  15534  incexclem  15557  divrcnv  15573  flo1  15575  fprodrev  15696  fprod2dlem  15699  ruclem6  15953  moddvds  15983  dvdsaddre2b  16025  dvdsflip  16035  addmodlteqALT  16043  nn0o  16101  fldivndvdslt  16132  bitsf1ocnv  16160  bitsf1  16162  sadcaddlem  16173  bezoutlem2  16257  bezoutlem4  16259  lcmgcdlem  16320  prmind2  16399  isprm5  16421  isprm6  16428  prmdvdsncoprmbd  16440  cncongrprm  16442  hashdvds  16485  crth  16488  eulerthlem2  16492  prmdiveq  16496  hashgcdlem  16498  hashgcdeq  16499  iserodd  16545  pclem  16548  pcprendvds2  16551  pcexp  16569  pcneg  16584  pc2dvds  16589  pcmpt  16602  prmpwdvds  16614  pockthg  16616  prmreclem5  16630  4sqlem11  16665  ramub2  16724  ramubcl  16728  ram0  16732  ramub1lem2  16737  ramcl  16739  prmgaplem3  16763  prmgaplem6  16766  setscom  16890  sscpwex  17536  initoeu2  17740  setcinv  17814  funcestrcsetclem9  17874  funcsetcestrclem9  17889  fullsetcestrc  17892  1stfcl  17923  2ndfcl  17924  hofpropd  17994  isacs3lem  18269  isacs4lem  18271  acsmap2d  18282  submnd0  18423  subsubm  18464  insubm  18466  frmdup1  18512  frmdup3lem  18514  sgrp2nmndlem2  18572  isgrpinv  18641  subsubg  18787  cycsubgcl  18834  conjghm  18874  qusghm  18880  gsumwrev  18982  gsmsymgrfixlem1  19044  symgfixelsi  19052  symgsssg  19084  symgfisg  19085  psgnunilem2  19112  odf1o2  19187  sylow1lem1  19212  odcau  19218  pgpfi  19219  pgpssslw  19228  fislw  19239  efgtlen  19341  efginvrel2  19342  efgrelexlemb  19365  efgredeu  19367  efgcpbllemb  19370  frgpup1  19390  cygablOLD  19501  lt6abl  19505  gsum2d  19582  gsum2d2lem  19583  gsum2d2  19584  telgsumfzslem  19598  dmdprdsplit2lem  19657  ablfacrp  19678  pgpfac1lem3  19689  gsummgp0  19856  irredrmul  19958  subsubrg  20059  islss4  20233  lspextmo  20327  lspsnat  20416  prmirredlem  20703  znf1o  20768  znidomb  20778  frgpcyg  20790  psgnghm  20794  psgndiflemB  20814  frlmlbs  21013  frlmup1  21014  lindfind  21032  islindf3  21042  lindfmm  21043  issubassa3  21081  resspsradd  21194  resspsrmul  21195  coe1tmmul2  21456  pf1ind  21530  mamulid  21599  mat1dimelbas  21629  mdetdiaglem  21756  mdetralt2  21767  mndifsplit  21794  smadiadetglem2  21830  1elcpmat  21873  pmatcollpw3lem  21941  chfacfisf  22012  chfacfisfcpmat  22013  chfacffsupp  22014  chfacfscmulfsupp  22017  chfacfscmulgsum  22018  chfacfpmmulfsupp  22021  chfacfpmmulgsum  22022  chfacfpmmulgsum2  22023  cayhamlem1  22024  cpmadugsumlemF  22034  cayleyhamilton1  22050  tgcl  22128  pptbas  22167  clsval2  22210  mretopd  22252  lmbr2  22419  cncls2  22433  nrmsep  22517  regsep2  22536  cmpsublem  22559  cmpsub  22560  tgcmp  22561  uncmp  22563  hauscmplem  22566  iunconnlem  22587  1stcrest  22613  2ndcctbss  22615  2ndcsep  22619  dis2ndc  22620  hausllycmp  22654  dislly  22657  kgentopon  22698  1stckgen  22714  kgencn3  22718  ptpjpre1  22731  ptbasin  22737  ptpjopn  22772  dfac14  22778  ptcnplem  22781  txcn  22786  txindis  22794  txdis1cn  22795  ptrescn  22799  txcmplem1  22801  txcmp  22803  txhaus  22807  txlm  22808  tx1stc  22810  txkgen  22812  xkococn  22820  qtopcn  22874  kqreglem1  22901  kqreglem2  22902  kqnrmlem1  22903  kqnrmlem2  22904  hmeoimaf1o  22930  reghmph  22953  nrmhmph  22954  txhmeo  22963  ptuncnv  22967  filconn  23043  fbasrn  23044  fmfnfmlem2  23115  flimfnfcls  23188  cnpfcfi  23200  alexsublem  23204  alexsubALTlem2  23208  alexsubALTlem3  23209  alexsubALTlem4  23210  alexsubALT  23211  ptcmplem3  23214  cnextfval  23222  tsmsxp  23315  imasdsf1olem  23535  bl2in  23562  blssps  23586  blss  23587  blssexps  23588  blssex  23589  blcld  23670  stdbdxmet  23680  met1stc  23686  prdsxmslem2  23694  metcnp3  23705  metcnpi3  23711  txmetcnp  23712  nmo0  23908  nmoid  23915  icccmplem1  23994  icccmp  23997  xrge0tsms  24006  metdseq0  24026  cnheiborlem  24126  cnheibor  24127  cnllycmp  24128  pcoval2  24188  cmetcaulem  24461  iscmet3lem1  24464  iscmet3lem2  24465  equivcau  24473  lmcau  24486  cncmet  24495  ivthlem2  24625  ivthlem3  24626  ovoliunlem2  24676  ovolscalem2  24687  uniioombl  24762  dyaddisj  24769  opnmbllem  24774  volivth  24780  ismbfd  24812  ismbf3d  24827  mbfimaopnlem  24828  mbfinf  24838  itg1addlem4  24872  itg1addlem4OLD  24873  mbfi1fseqlem1  24889  mbfi1fseqlem3  24891  mbfi1fseqlem4  24892  mbfi1fseqlem5  24893  mbfi1fseqlem6  24894  itg2seq  24916  itg2lea  24918  itg2split  24923  itg2cnlem1  24935  bddiblnc  25015  limciun  25067  dvmptfsum  25148  rolle  25163  c1lip1  25170  dvcnvrelem1  25190  dvcnvre  25192  dvcvx  25193  itgsubst  25222  tdeglem4  25233  tdeglem4OLD  25234  mdegmullem  25252  plyco0  25362  coemullem  25420  dgreq0  25435  dgrmul  25440  dgrco  25445  elqaalem2  25489  aannenlem1  25497  aaliou3lem9  25519  ulmres  25556  ulmshftlem  25557  angneg  25962  dcubic  26005  cxploglim  26136  cxploglim2  26137  scvxcvx  26144  lgamgulmlem5  26191  lgamcvg2  26213  ftalem2  26232  basellem3  26241  basellem4  26242  sqff1o  26340  fsumdvdsdiaglem  26341  dvdsflsumcom  26346  dvdsmulf1o  26352  fsumvma2  26371  logfac2  26374  logfacrlim  26381  logexprlim  26382  dchrelbasd  26396  lgsne0  26492  lgsqrlem2  26504  lgsqrmodndvds  26510  gausslemma2dlem1a  26522  lgseisenlem2  26533  lgsquadlem1  26537  lgsquadlem2  26538  lgsquadlem3  26539  lgsquad2lem2  26542  2sqlem8  26583  2sqlem11  26586  2sqreultlem  26604  2sqreunnltlem  26607  chpo1ubb  26638  vmadivsum  26639  rplogsumlem2  26642  rpvmasumlem  26644  dchrmusum2  26651  dchrvmasumlem1  26652  dchrisum0fno1  26668  dchrisum0re  26670  dchrisum0lem1  26673  dchrisum0lem2  26675  dchrisum0lem3  26676  dchrisum0  26677  mulogsumlem  26688  mulog2sumlem2  26692  vmalogdivsum2  26695  logsqvma  26699  log2sumbnd  26701  selberglem3  26704  selberg  26705  selberg2lem  26707  selberg2b  26709  selberg3lem2  26715  pntrmax  26721  pntrsumo1  26722  pntlemn  26757  pntlemp  26767  qabvle  26782  ostthlem1  26784  ostthlem2  26785  ostth2lem2  26791  ostth3  26795  idmot  26907  brbtwn2  27282  colinearalglem4  27286  colinearalg  27287  ax5seglem9  27314  axpaschlem  27317  axcontlem2  27342  axcontlem7  27347  axcontlem8  27348  eengtrkg  27363  upgr1eopALT  27496  uspgredg2vlem  27599  subumgr  27664  nbgr0vtxlem  27731  edgnbusgreu  27743  nb3grprlem1  27756  wlkl1loop  28014  pthdivtx  28106  usgr2pth  28141  crctcshwlkn0  28195  wlklnwwlkln1  28242  wwlksnext  28267  clwwlkccatlem  28362  clwlkclwwlklem2a  28371  clwwlkinwwlk  28413  clwwlkn1loopb  28416  clwwlkf  28420  wwlksext2clwwlk  28430  wwlksubclwwlk  28431  clwwlknscsh  28435  clwwlknon1  28470  clwwlknonex2e  28483  1conngr  28567  n4cyclfrgr  28664  numclwwlk2lem1lem  28715  2clwwlk2clwwlk  28723  numclwwlk1lem2f1  28730  numclwlk1lem1  28742  numclwwlk2lem1  28749  numclwlk2lem2f  28750  numclwwlk7  28764  frgrogt3nreg  28770  grpoidinvlem1  28875  grpoidinvlem3  28877  grporcan  28889  nmlnoubi  29167  blocnilem  29175  ipblnfi  29226  htthlem  29288  ocsh  29654  shmodsi  29760  pjhthlem2  29763  5oalem2  30026  eigposi  30207  nmopub2tALT  30280  nmfnleub2  30297  nmcexi  30397  nmopcoi  30466  kbass3  30489  mdslmd1lem1  30696  mdslmd1lem2  30697  chirredlem2  30762  chirredlem4  30764  mdsymlem3  30776  mdsymlem5  30778  sumdmdii  30786  sumdmdlem  30789  sumdmdlem2  30790  foresf1o  30859  disjxpin  30936  1stpreimas  31047  resf1o  31074  nn0xmulclb  31103  wrdt2ind  31234  xrge0tsmsd  31326  gsumvsca1  31488  gsumvsca2  31489  islinds5  31572  mdetpmtr1  31782  mdetpmtr2  31783  pstmxmet  31856  qqhghm  31947  qqhrhm  31948  esumpcvgval  32055  volmeas  32208  imambfm  32238  dya2iocnrect  32257  oddpwdc  32330  sseqf  32368  orvcgteel  32443  orvclteel  32448  ballotlemsf1o  32489  bnj1110  32971  bnj1118  32973  f1resveqaeq  33066  txpconn  33203  connpconn  33206  cnllysconn  33216  rellysconn  33222  cvmsss2  33245  cvmlift2lem9  33282  satf00  33345  fmlasuc  33357  mrsubfval  33479  mppsval  33543  dfon2lem6  33773  frxp2  33800  poxp3  33805  frxp3  33806  wzel  33827  sltres  33874  nosupno  33915  nosupbnd2  33928  noinfno  33930  noinfbnd2  33943  etasslt  34016  ifscgr  34355  cgrxfr  34366  btwnconn1lem5  34402  btwnconn1lem6  34403  btwnconn1lem12  34409  brsegle  34419  finminlem  34516  nn0prpwlem  34520  fnessref  34555  refssfne  34556  neibastop1  34557  topjoin  34563  fnemeet2  34565  bj-prmoore  35295  bj-finsumval0  35465  topdifinffinlem  35527  lindsadd  35779  matunitlindflem2  35783  poimirlem28  35814  poimirlem32  35818  opnmbllem0  35822  mblfinlem1  35823  mblfinlem4  35826  ismblfin  35827  mbfresfi  35832  itg2addnclem  35837  itg2addnclem3  35839  itg2addnc  35840  unirep  35880  frinfm  35902  sdclem2  35909  geomcau  35926  istotbnd3  35938  sstotbnd2  35941  sstotbnd  35942  sstotbnd3  35943  totbndbnd  35956  cntotbnd  35963  ismtyres  35975  heibor1lem  35976  heiborlem1  35978  heiborlem8  35985  ismndo1  36040  isdivrngo  36117  unichnidl  36198  erim2  36796  cvlcvr1  37360  ishlat3N  37375  llnmlplnN  37560  islvol2aN  37613  4atlem4c  37622  4atlem4d  37623  isline2  37795  isline3  37797  linepsubclN  37972  lhpexle3lem  38032  lhpjat2  38042  cdlemd4  38222  cdleme0cq  38236  cdleme32fva  38458  cdleme32fvaw  38460  tendo0mul  38847  tendo0mulr  38848  diameetN  39077  dvhvaddcl  39116  dvhvaddcomN  39117  cdlemm10N  39139  dvadiaN  39149  djavalN  39156  dihvalcqat  39260  dihopelvalcpre  39269  djhval  39419  dihjat1lem  39449  sticksstones11  40119  sticksstones22  40131  metakunt15  40146  metakunt16  40147  evlsbagval  40282  fsuppind  40286  mhpind  40290  mhphf  40292  remul01  40397  prjspertr  40451  prjsprellsp  40457  elrfi  40523  nacsfix  40541  fzsplit1nn0  40583  eldioph2  40591  lzenom  40599  irrapxlem3  40653  pellexlem5  40662  pell1234qrne0  40682  pell1234qrmulcl  40684  pell14qrdich  40698  pell1qrge1  40699  pellqrex  40708  reglogltb  40720  reglogleb  40721  rmxypairf1o  40740  rmxycomplete  40746  monotoddzzfi  40771  congadd  40795  congsym  40797  acongrep  40809  jm2.19lem3  40820  jm2.19lem4  40821  jm2.22  40824  jm2.25  40828  expdiophlem1  40850  wepwsolem  40874  kelac1  40895  lmhmfgsplit  40918  pwslnm  40926  hbtlem6  40961  hbt  40962  mon1psubm  41038  deg1mhm  41039  fzunt  41069  fzuntd  41070  fzunt1d  41071  fzuntgd  41072  iunrelexp0  41317  dssmapnvod  41635  gsumws3  41814  gsumws4  41815  mulltgt0  42572  fnchoice  42579  disjrnmpt2  42733  fzisoeu  42846  fsumiunss  43123  climinf  43154  mullimc  43164  mullimcf  43171  stoweidlem14  43562  stoweidlem17  43565  stoweidlem34  43582  stoweidlem50  43598  fourierdlem42  43697  fourierdlem62  43716  fourierdlem71  43725  fourierdlem76  43730  qndenserrnbllem  43842  subsaliuncl  43904  sge0resplit  43951  2reu8i  44616  fundcmpsurinjpreimafv  44871  iccpartigtl  44886  prproropf1olem2  44967  prproropf1olem4  44969  paireqne  44974  prmdvdsfmtnof1lem2  45048  bgoldbtbndlem3  45270  bgoldbtbnd  45272  isomushgr  45289  isomuspgrlem2c  45293  uspgrsprf1  45320  subsubmgm  45362  isassintop  45415  2zlidl  45503  2zrngnmrid  45519  rngcinv  45550  rngcinvALTV  45562  ringcinv  45601  funcringcsetcALTV2lem9  45613  ringcinvALTV  45625  funcringcsetclem9ALTV  45636  fldhmsubc  45653  fldhmsubcALTV  45671  mndpsuppss  45718  gsumlsscl  45730  lincsum  45781  lindslinindsimp1  45809  lindslinindimp2lem4  45813  lincresunitlem2  45828  elfzolborelfzop1  45871  elbigo2  45909  digexp  45964  dig1  45965  nn0sumshdiglemB  45977  1arymaptf1  45999  2arymaptf1  46010  itcoval1  46020  itcoval2  46021  itcoval3  46022  itcovalsucov  46025  ackvalsuc1mpt  46035  itschlc0xyqsol  46124  thincciso  46341  indthinc  46344  indthincALT  46345