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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simprl  769  simprll  777  simprlr  778  simprl1  1214  simprl2  1215  simprl3  1216  disjxiun  5065  reusv2lem4  5304  axprlem5  5330  fr2nr  5535  somin1  5995  tz7.7  6219  f1oprg  6661  soisores  7082  elovmporab1w  7394  elovmporab1  7395  sorpssi  7457  onint  7512  ordsucelsuc  7539  elxp5  7630  wemoiso  7676  wemoiso2  7677  el2xptp0  7738  ressuppss  7851  imacosuppOLD  7877  tz7.48lem  8079  oalimcl  8188  oeeui  8230  oaabs2  8274  omabs  8276  swoer  8321  ralxpmap  8462  pw2f1olem  8623  enfixsn  8628  mapxpen  8685  mapunen  8688  unxpdomlem2  8725  unxpdomlem3  8726  findcard3  8763  isfinite2  8778  domunfican  8793  fodomfi  8799  fissuni  8831  fipreima  8832  indexfi  8834  fsuppsssupp  8851  marypha1lem  8899  marypha2  8905  supmo  8918  infmo  8961  oieu  9005  brwdom2  9039  ixpiunwdom  9057  cantnfval2  9134  cantnfle  9136  cantnflt  9137  cantnf  9158  wemapwe  9162  cnfcom  9165  rankonidlem  9259  r1pwcl  9278  eldju2ndl  9355  eldju2ndr  9356  djuun  9357  infxpenlem  9441  infxpenc2lem1  9447  fseqenlem1  9452  dfac8clem  9460  mappwen  9540  dfac3  9549  dfac5  9556  dfac12lem3  9573  infunsdom  9638  coftr  9697  ssfin4  9734  domfin4  9735  fin23lem26  9749  fin23lem22  9751  fin23lem28  9764  fin23lem32  9768  fin23lem40  9775  isf32lem5  9781  compssiso  9798  isf34lem4  9801  isfin1-3  9810  fin1a2lem13  9836  hsmexlem2  9851  hsmexlem4  9853  zorn2lem1  9920  ttukeylem6  9938  iundom2g  9964  konigthlem  9992  pwcfsdom  10007  fpwwe2lem12  10065  fpwwe2  10067  pwfseqlem3  10084  winalim2  10120  r1wunlim  10161  inttsk  10198  inar1  10199  grur1  10244  nqereq  10359  ltexprlem7  10466  prlem936  10471  00id  10817  addid2  10825  ltord1  11168  divdiv1  11353  divdiv2  11354  conjmul  11359  ltdivmul  11517  ledivmul  11518  lt2mul2div  11520  ltdiv23  11533  lediv23  11534  lediv12a  11535  ledivp1  11544  negfi  11591  nn0nndivcl  11969  nn0ge0div  12054  peano2uz2  12073  peano5uzi  12074  eluzp1m1  12271  qbtwnre  12595  xralrple  12601  xleadd1a  12649  xmulge0  12680  xmulass  12683  xlemul1a  12684  iooshf  12818  divelunit  12883  eluzgtdifelfzo  13102  modadd1  13279  modmul1  13295  seqcl2  13391  seqfveq2  13395  seqid2  13419  seqhomo  13420  seqdistr  13424  mulexpz  13472  leexp2r  13541  expnlbnd2  13598  expmulnbnd  13599  hashmap  13799  hashfun  13801  hashbclem  13813  hashfacen  13815  hashf1lem2  13817  hashf1  13818  ccatsymb  13938  swrdwrdsymb  14026  swrdsb0eq  14027  ccatpfx  14065  swrdswrd  14069  wrdind  14086  wrd2ind  14087  swrdccatin1  14089  swrdccatin2  14093  pfxccatin12lem2  14095  pfxccatin12  14097  swrdccat  14099  repswswrd  14148  0csh0  14157  cshwidxmod  14167  2cshw  14177  cshweqrep  14185  relexp0g  14383  relexpsucnnr  14386  relexpindlem  14424  sqrlem1  14604  sqrlem6  14609  rlim  14854  rlimclim1  14904  climsup  15028  caurcvg2  15036  caucvgb  15038  iseralt  15043  sumss  15083  fsum2dlem  15127  mptfzshft  15135  modfsummod  15151  o1fsum  15170  incexclem  15193  divrcnv  15209  flo1  15211  fprodrev  15333  fprod2dlem  15336  ruclem6  15590  moddvds  15620  dvdsaddre2b  15659  dvdsflip  15669  addmodlteqALT  15677  nn0o  15736  fldivndvdslt  15767  bitsf1ocnv  15795  bitsf1  15797  sadcaddlem  15808  bezoutlem2  15890  bezoutlem4  15892  lcmgcdlem  15952  prmind2  16031  isprm5  16053  isprm6  16060  cncongrprm  16071  hashdvds  16114  crth  16117  eulerthlem2  16121  prmdiveq  16125  hashgcdlem  16127  hashgcdeq  16128  iserodd  16174  pclem  16177  pcprendvds2  16180  pcexp  16198  pcneg  16212  pc2dvds  16217  pcmpt  16230  prmpwdvds  16242  pockthg  16244  prmreclem5  16258  4sqlem11  16293  ramub2  16352  ramubcl  16356  ram0  16360  ramub1lem2  16365  ramcl  16367  prmgaplem3  16391  prmgaplem6  16394  setscom  16529  sscpwex  17087  initoeu2  17278  setcinv  17352  funcestrcsetclem9  17400  funcsetcestrclem9  17415  fullsetcestrc  17418  1stfcl  17449  2ndfcl  17450  hofpropd  17519  isacs3lem  17778  isacs4lem  17780  acsmap2d  17791  submnd0  17942  subsubm  17983  insubm  17985  frmdup1  18031  frmdup3lem  18033  sgrp2nmndlem2  18091  isgrpinv  18158  subsubg  18304  cycsubgcl  18351  conjghm  18391  qusghm  18397  gsumwrev  18496  gsmsymgrfixlem1  18557  symgfixelsi  18565  symgsssg  18597  symgfisg  18598  psgnunilem2  18625  odf1o2  18700  sylow1lem1  18725  odcau  18731  pgpfi  18732  pgpssslw  18741  fislw  18752  efgtlen  18854  efginvrel2  18855  efgrelexlemb  18878  efgredeu  18880  efgcpbllemb  18883  frgpup1  18903  cygablOLD  19013  lt6abl  19017  gsum2d  19094  gsum2d2lem  19095  gsum2d2  19096  telgsumfzslem  19110  dmdprdsplit2lem  19169  ablfacrp  19190  pgpfac1lem3  19201  gsummgp0  19360  irredrmul  19459  subsubrg  19563  islss4  19736  lspextmo  19830  lspsnat  19919  issubassa3  20099  resspsradd  20198  resspsrmul  20199  coe1tmmul2  20446  pf1ind  20520  prmirredlem  20642  znf1o  20700  znidomb  20710  frgpcyg  20722  psgnghm  20726  psgndiflemB  20746  frlmlbs  20943  frlmup1  20944  lindfind  20962  islindf3  20972  lindfmm  20973  mamulid  21052  mat1dimelbas  21082  mdetdiaglem  21209  mdetralt2  21220  mndifsplit  21247  smadiadetglem2  21283  1elcpmat  21325  pmatcollpw3lem  21393  chfacfisf  21464  chfacfisfcpmat  21465  chfacffsupp  21466  chfacfscmulfsupp  21469  chfacfscmulgsum  21470  chfacfpmmulfsupp  21473  chfacfpmmulgsum  21474  chfacfpmmulgsum2  21475  cayhamlem1  21476  cpmadugsumlemF  21486  cayleyhamilton1  21502  tgcl  21579  pptbas  21618  clsval2  21660  mretopd  21702  lmbr2  21869  cncls2  21883  nrmsep  21967  regsep2  21986  cmpsublem  22009  cmpsub  22010  tgcmp  22011  uncmp  22013  hauscmplem  22016  iunconnlem  22037  1stcrest  22063  2ndcctbss  22065  2ndcsep  22069  dis2ndc  22070  hausllycmp  22104  dislly  22107  kgentopon  22148  1stckgen  22164  kgencn3  22168  ptpjpre1  22181  ptbasin  22187  ptpjopn  22222  dfac14  22228  ptcnplem  22231  txcn  22236  txindis  22244  txdis1cn  22245  ptrescn  22249  txcmplem1  22251  txcmp  22253  txhaus  22257  txlm  22258  tx1stc  22260  txkgen  22262  xkococn  22270  qtopcn  22324  kqreglem1  22351  kqreglem2  22352  kqnrmlem1  22353  kqnrmlem2  22354  hmeoimaf1o  22380  reghmph  22403  nrmhmph  22404  txhmeo  22413  ptuncnv  22417  filconn  22493  fbasrn  22494  fmfnfmlem2  22565  flimfnfcls  22638  cnpfcfi  22650  alexsublem  22654  alexsubALTlem2  22658  alexsubALTlem3  22659  alexsubALTlem4  22660  alexsubALT  22661  ptcmplem3  22664  cnextfval  22672  tsmsxp  22765  imasdsf1olem  22985  bl2in  23012  blssps  23036  blss  23037  blssexps  23038  blssex  23039  blcld  23117  stdbdxmet  23127  met1stc  23133  prdsxmslem2  23141  metcnp3  23152  metcnpi3  23158  txmetcnp  23159  nmo0  23346  nmoid  23353  icccmplem1  23432  icccmp  23435  xrge0tsms  23444  metdseq0  23464  cnheiborlem  23560  cnheibor  23561  cnllycmp  23562  pcoval2  23622  cmetcaulem  23893  iscmet3lem1  23896  iscmet3lem2  23897  equivcau  23905  lmcau  23918  cncmet  23927  ivthlem2  24055  ivthlem3  24056  ovoliunlem2  24106  ovolscalem2  24117  uniioombl  24192  dyaddisj  24199  opnmbllem  24204  volivth  24210  ismbfd  24242  ismbf3d  24257  mbfimaopnlem  24258  mbfinf  24268  itg1addlem4  24302  mbfi1fseqlem1  24318  mbfi1fseqlem3  24320  mbfi1fseqlem4  24321  mbfi1fseqlem5  24322  mbfi1fseqlem6  24323  itg2seq  24345  itg2lea  24347  itg2split  24352  itg2cnlem1  24364  limciun  24494  dvmptfsum  24574  rolle  24589  c1lip1  24596  dvcnvrelem1  24616  dvcnvre  24618  dvcvx  24619  itgsubst  24648  tdeglem4  24656  mdegmullem  24674  plyco0  24784  coemullem  24842  dgreq0  24857  dgrmul  24862  dgrco  24867  elqaalem2  24911  aannenlem1  24919  aaliou3lem9  24941  ulmres  24978  ulmshftlem  24979  angneg  25383  dcubic  25426  cxploglim  25557  cxploglim2  25558  scvxcvx  25565  lgamgulmlem5  25612  lgamcvg2  25634  ftalem2  25653  basellem3  25662  basellem4  25663  sqff1o  25761  fsumdvdsdiaglem  25762  dvdsflsumcom  25767  dvdsmulf1o  25773  fsumvma2  25792  logfac2  25795  logfacrlim  25802  logexprlim  25803  dchrelbasd  25817  lgsne0  25913  lgsqrlem2  25925  lgsqrmodndvds  25931  gausslemma2dlem1a  25943  lgseisenlem2  25954  lgsquadlem1  25958  lgsquadlem2  25959  lgsquadlem3  25960  lgsquad2lem2  25963  2sqlem8  26004  2sqlem11  26007  2sqreultlem  26025  2sqreunnltlem  26028  chpo1ubb  26059  vmadivsum  26060  rplogsumlem2  26063  rpvmasumlem  26065  dchrmusum2  26072  dchrvmasumlem1  26073  dchrisum0fno1  26089  dchrisum0re  26091  dchrisum0lem1  26094  dchrisum0lem2  26096  dchrisum0lem3  26097  dchrisum0  26098  mulogsumlem  26109  mulog2sumlem2  26113  vmalogdivsum2  26116  logsqvma  26120  log2sumbnd  26122  selberglem3  26125  selberg  26126  selberg2lem  26128  selberg2b  26130  selberg3lem2  26136  pntrmax  26142  pntrsumo1  26143  pntlemn  26178  pntlemp  26188  qabvle  26203  ostthlem1  26205  ostthlem2  26206  ostth2lem2  26212  ostth3  26216  idmot  26325  brbtwn2  26693  colinearalglem4  26697  colinearalg  26698  ax5seglem9  26725  axpaschlem  26728  axcontlem2  26753  axcontlem7  26758  axcontlem8  26759  eengtrkg  26774  upgr1eopALT  26904  uspgredg2vlem  27007  subumgr  27072  nbgr0vtxlem  27139  edgnbusgreu  27151  nb3grprlem1  27164  wlkl1loop  27421  pthdivtx  27512  usgr2pth  27547  crctcshwlkn0  27601  wlklnwwlkln1  27648  wwlksnext  27673  clwwlkccatlem  27769  clwlkclwwlklem2a  27778  clwwlkinwwlk  27820  clwwlkn1loopb  27823  clwwlkf  27828  wwlksext2clwwlk  27838  wwlksubclwwlk  27839  clwwlknscsh  27843  clwwlknon1  27878  clwwlknonex2e  27891  1conngr  27975  n4cyclfrgr  28072  numclwwlk2lem1lem  28123  2clwwlk2clwwlk  28131  numclwwlk1lem2f1  28138  numclwlk1lem1  28150  numclwwlk2lem1  28157  numclwlk2lem2f  28158  numclwwlk7  28172  frgrogt3nreg  28178  grpoidinvlem1  28283  grpoidinvlem3  28285  grporcan  28297  nmlnoubi  28575  blocnilem  28583  ipblnfi  28634  htthlem  28696  ocsh  29062  shmodsi  29168  pjhthlem2  29171  5oalem2  29434  eigposi  29615  nmopub2tALT  29688  nmfnleub2  29705  nmcexi  29805  nmopcoi  29874  kbass3  29897  mdslmd1lem1  30104  mdslmd1lem2  30105  chirredlem2  30170  chirredlem4  30172  mdsymlem3  30184  mdsymlem5  30186  sumdmdii  30194  sumdmdlem  30197  sumdmdlem2  30198  foresf1o  30267  disjxpin  30340  1stpreimas  30443  resf1o  30468  nn0xmulclb  30498  wrdt2ind  30629  xrge0tsmsd  30694  gsumvsca1  30856  gsumvsca2  30857  islinds5  30934  mdetpmtr1  31090  mdetpmtr2  31091  pstmxmet  31139  qqhghm  31231  qqhrhm  31232  esumpcvgval  31339  volmeas  31492  imambfm  31522  dya2iocnrect  31541  oddpwdc  31614  sseqf  31652  orvcgteel  31727  orvclteel  31732  ballotlemsf1o  31773  bnj1110  32256  bnj1118  32258  f1resveqaeq  32360  txpconn  32481  connpconn  32484  cnllysconn  32494  rellysconn  32500  cvmsss2  32523  cvmlift2lem9  32560  satf00  32623  fmlasuc  32635  mrsubfval  32757  mppsval  32821  dfon2lem6  33035  trpredmintr  33072  wzel  33113  fprlem1  33139  frrlem15  33144  sltres  33171  nosupno  33205  nosupbnd2  33218  sslttr  33270  ifscgr  33507  cgrxfr  33518  btwnconn1lem5  33554  btwnconn1lem6  33555  btwnconn1lem12  33561  brsegle  33571  finminlem  33668  nn0prpwlem  33672  fnessref  33707  refssfne  33708  neibastop1  33709  topjoin  33715  fnemeet2  33717  bj-prmoore  34409  bj-imdirid  34477  bj-finsumval0  34569  topdifinffinlem  34630  lindsadd  34887  matunitlindflem2  34891  poimirlem28  34922  poimirlem32  34926  opnmbllem0  34930  mblfinlem1  34931  mblfinlem4  34934  ismblfin  34935  mbfresfi  34940  itg2addnclem  34945  itg2addnclem3  34947  itg2addnc  34948  bddiblnc  34964  unirep  34990  frinfm  35012  sdclem2  35019  geomcau  35036  istotbnd3  35051  sstotbnd2  35054  sstotbnd  35055  sstotbnd3  35056  totbndbnd  35069  cntotbnd  35076  ismtyres  35088  heibor1lem  35089  heiborlem1  35091  heiborlem8  35098  ismndo1  35153  isdivrngo  35230  unichnidl  35311  erim2  35913  cvlcvr1  36477  ishlat3N  36492  llnmlplnN  36677  islvol2aN  36730  4atlem4c  36739  4atlem4d  36740  isline2  36912  isline3  36914  linepsubclN  37089  lhpexle3lem  37149  lhpjat2  37159  cdlemd4  37339  cdleme0cq  37353  cdleme32fva  37575  cdleme32fvaw  37577  tendo0mul  37964  tendo0mulr  37965  diameetN  38194  dvhvaddcl  38233  dvhvaddcomN  38234  cdlemm10N  38256  dvadiaN  38266  djavalN  38273  dihvalcqat  38377  dihopelvalcpre  38386  djhval  38536  dihjat1lem  38566  remul01  39244  prjspertr  39262  prjsprellsp  39268  elrfi  39298  nacsfix  39316  fzsplit1nn0  39358  eldioph2  39366  lzenom  39374  irrapxlem3  39428  pellexlem5  39437  pell1234qrne0  39457  pell1234qrmulcl  39459  pell14qrdich  39473  pell1qrge1  39474  pellqrex  39483  reglogltb  39495  reglogleb  39496  rmxypairf1o  39515  rmxycomplete  39521  monotoddzzfi  39546  congadd  39570  congsym  39572  acongrep  39584  jm2.19lem3  39595  jm2.19lem4  39596  jm2.22  39599  jm2.25  39603  expdiophlem1  39625  wepwsolem  39649  kelac1  39670  lmhmfgsplit  39693  pwslnm  39701  hbtlem6  39736  hbt  39737  mon1psubm  39813  deg1mhm  39814  iunrelexp0  40054  dssmapnvod  40373  gsumws3  40556  gsumws4  40557  mulltgt0  41286  fnchoice  41293  disjrnmpt2  41456  fzisoeu  41574  fsumiunss  41863  climinf  41894  mullimc  41904  mullimcf  41911  stoweidlem14  42306  stoweidlem17  42309  stoweidlem34  42326  stoweidlem50  42342  fourierdlem42  42441  fourierdlem62  42460  fourierdlem71  42469  fourierdlem76  42474  qndenserrnbllem  42586  subsaliuncl  42648  sge0resplit  42695  2reu8i  43319  fundcmpsurinjpreimafv  43575  iccpartigtl  43590  prproropf1olem2  43673  prproropf1olem4  43675  paireqne  43680  prmdvdsfmtnof1lem2  43754  bgoldbtbndlem3  43979  bgoldbtbnd  43981  isomushgr  43998  isomuspgrlem2c  44002  uspgrsprf1  44029  subsubmgm  44071  isassintop  44124  2zlidl  44212  2zrngnmrid  44228  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  funcringcsetcALTV2lem9  44322  ringcinvALTV  44334  funcringcsetclem9ALTV  44345  fldhmsubc  44362  fldhmsubcALTV  44380  mndpsuppss  44426  gsumlsscl  44438  lincsum  44491  lindslinindsimp1  44519  lindslinindimp2lem4  44523  lincresunitlem2  44538  elfzolborelfzop1  44581  elbigo2  44619  digexp  44674  dig1  44675  nn0sumshdiglemB  44687  itschlc0xyqsol  44761