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 482	. 2 ⊢ ((𝜒 ∧ 𝜑) → 𝜓)
3	2	adantrr 715	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  769  simprll  777  simprlr  778  simprl1  1218  simprl2  1219  simprl3  1220  disjxiun  5145  reusv2lem4  5399  axprlem5  5425  fr2nr  5654  somin1  6134  tz7.7  6390  f1oprg  6878  soisores  7323  elovmporab1w  7652  elovmporab1  7653  sorpssi  7718  onint  7777  ordsucelsuc  7809  elxp5  7913  wemoiso  7959  wemoiso2  7960  el2xptp0  8021  frxp2  8129  frxp3  8136  ressuppss  8167  fprlem1  8284  tz7.48lem  8440  oalimcl  8559  oeeui  8601  oaabs2  8647  omabs  8649  swoer  8732  ralxpmap  8889  pw2f1olem  9075  enfixsn  9080  mapxpen  9142  mapunen  9145  php  9209  unxpdomlem2  9250  unxpdomlem3  9251  findcard3OLD  9285  isfinite2  9300  domunfican  9319  fodomfi  9324  fissuni  9356  fipreima  9357  indexfi  9359  fsuppsssupp  9378  marypha1lem  9427  marypha2  9433  supmo  9446  infmo  9489  oieu  9533  brwdom2  9567  ixpiunwdom  9584  cantnfval2  9663  cantnfle  9665  cantnflt  9666  cantnf  9687  wemapwe  9691  cnfcom  9694  frrlem15  9751  rankonidlem  9822  r1pwcl  9841  eldju2ndl  9918  eldju2ndr  9919  djuun  9920  infxpenlem  10007  infxpenc2lem1  10013  fseqenlem1  10018  dfac8clem  10026  mappwen  10106  dfac3  10115  dfac5  10122  dfac12lem3  10139  infunsdom  10208  coftr  10267  ssfin4  10304  domfin4  10305  fin23lem26  10319  fin23lem22  10321  fin23lem28  10334  fin23lem32  10338  fin23lem40  10345  isf32lem5  10351  compssiso  10368  isf34lem4  10371  isfin1-3  10380  fin1a2lem13  10406  hsmexlem2  10421  hsmexlem4  10423  zorn2lem1  10490  ttukeylem6  10508  iundom2g  10534  konigthlem  10562  pwcfsdom  10577  fpwwe2lem11  10635  fpwwe2  10637  pwfseqlem3  10654  winalim2  10690  r1wunlim  10731  inttsk  10768  inar1  10769  grur1  10814  nqereq  10929  ltexprlem7  11036  prlem936  11041  00id  11388  addlid  11396  ltord1  11739  divdiv1  11924  divdiv2  11925  conjmul  11930  ltdivmul  12088  ledivmul  12089  lt2mul2div  12091  ltdiv23  12104  lediv23  12105  lediv12a  12106  ledivp1  12115  negfi  12162  nn0nndivcl  12542  nn0ge0div  12630  peano2uz2  12649  peano5uzi  12650  eluzp1m1  12847  qbtwnre  13177  xralrple  13183  xleadd1a  13231  xmulge0  13262  xmulass  13265  xlemul1a  13266  iooshf  13402  divelunit  13470  eluzgtdifelfzo  13693  modadd1  13872  modmul1  13888  seqcl2  13985  seqfveq2  13989  seqid2  14013  seqhomo  14014  seqdistr  14018  mulexpz  14067  leexp2r  14138  expnlbnd2  14196  expmulnbnd  14197  hashmap  14394  hashfun  14396  hashbclem  14410  hashfacen  14412  hashfacenOLD  14413  hashf1lem2  14416  hashf1  14417  ccatsymb  14531  swrdwrdsymb  14611  swrdsb0eq  14612  ccatpfx  14650  swrdswrd  14654  wrdind  14671  wrd2ind  14672  swrdccatin1  14674  swrdccatin2  14678  pfxccatin12lem2  14680  pfxccatin12  14682  swrdccat  14684  repswswrd  14733  0csh0  14742  cshwidxmod  14752  2cshw  14762  cshweqrep  14770  relexp0g  14968  relexpsucnnr  14971  relexpindlem  15009  01sqrexlem1  15188  01sqrexlem6  15193  rlim  15438  rlimclim1  15488  climsup  15615  caurcvg2  15623  caucvgb  15625  iseralt  15630  sumss  15669  fsum2dlem  15715  mptfzshft  15723  modfsummod  15739  o1fsum  15758  incexclem  15781  divrcnv  15797  flo1  15799  fprodrev  15920  fprod2dlem  15923  ruclem6  16177  moddvds  16207  dvdsaddre2b  16249  dvdsflip  16259  addmodlteqALT  16267  nn0o  16325  fldivndvdslt  16356  bitsf1ocnv  16384  bitsf1  16386  sadcaddlem  16397  bezoutlem2  16481  bezoutlem4  16483  lcmgcdlem  16542  prmind2  16621  isprm5  16643  isprm6  16650  prmdvdsncoprmbd  16662  cncongrprm  16664  hashdvds  16707  crth  16710  eulerthlem2  16714  prmdiveq  16718  hashgcdlem  16720  hashgcdeq  16721  iserodd  16767  pclem  16770  pcprendvds2  16773  pcexp  16791  pcneg  16806  pc2dvds  16811  pcmpt  16824  prmpwdvds  16836  pockthg  16838  prmreclem5  16852  4sqlem11  16887  ramub2  16946  ramubcl  16950  ram0  16954  ramub1lem2  16959  ramcl  16961  prmgaplem3  16985  prmgaplem6  16988  setscom  17112  sscpwex  17761  initoeu2  17965  setcinv  18039  funcestrcsetclem9  18099  funcsetcestrclem9  18114  fullsetcestrc  18117  1stfcl  18148  2ndfcl  18149  hofpropd  18219  isacs3lem  18494  isacs4lem  18496  acsmap2d  18507  submnd0  18653  subsubm  18696  insubm  18698  frmdup1  18744  frmdup3lem  18746  sgrp2nmndlem2  18804  isgrpinv  18877  subsubg  19028  cycsubgcl  19082  conjghm  19122  qusghm  19128  gsumwrev  19232  gsmsymgrfixlem1  19294  symgfixelsi  19302  symgsssg  19334  symgfisg  19335  psgnunilem2  19362  odf1o2  19440  sylow1lem1  19465  odcau  19471  pgpfi  19472  pgpssslw  19481  fislw  19492  efgtlen  19593  efginvrel2  19594  efgrelexlemb  19617  efgredeu  19619  efgcpbllemb  19622  frgpup1  19642  lt6abl  19762  gsum2d  19839  gsum2d2lem  19840  gsum2d2  19841  telgsumfzslem  19855  dmdprdsplit2lem  19914  ablfacrp  19935  pgpfac1lem3  19946  gsummgp0  20129  irredrmul  20240  subsubrg  20344  islss4  20572  lspextmo  20666  lspsnat  20757  prmirredlem  21041  znf1o  21106  znidomb  21116  frgpcyg  21128  psgnghm  21132  psgndiflemB  21152  frlmlbs  21351  frlmup1  21352  lindfind  21370  islindf3  21380  lindfmm  21381  issubassa3  21419  resspsradd  21535  resspsrmul  21536  coe1tmmul2  21797  pf1ind  21873  mamulid  21942  mat1dimelbas  21972  mdetdiaglem  22099  mdetralt2  22110  mndifsplit  22137  smadiadetglem2  22173  1elcpmat  22216  pmatcollpw3lem  22284  chfacfisf  22355  chfacfisfcpmat  22356  chfacffsupp  22357  chfacfscmulfsupp  22360  chfacfscmulgsum  22361  chfacfpmmulfsupp  22364  chfacfpmmulgsum  22365  chfacfpmmulgsum2  22366  cayhamlem1  22367  cpmadugsumlemF  22377  cayleyhamilton1  22393  tgcl  22471  pptbas  22510  clsval2  22553  mretopd  22595  lmbr2  22762  cncls2  22776  nrmsep  22860  regsep2  22879  cmpsublem  22902  cmpsub  22903  tgcmp  22904  uncmp  22906  hauscmplem  22909  iunconnlem  22930  1stcrest  22956  2ndcctbss  22958  2ndcsep  22962  dis2ndc  22963  hausllycmp  22997  dislly  23000  kgentopon  23041  1stckgen  23057  kgencn3  23061  ptpjpre1  23074  ptbasin  23080  ptpjopn  23115  dfac14  23121  ptcnplem  23124  txcn  23129  txindis  23137  txdis1cn  23138  ptrescn  23142  txcmplem1  23144  txcmp  23146  txhaus  23150  txlm  23151  tx1stc  23153  txkgen  23155  xkococn  23163  qtopcn  23217  kqreglem1  23244  kqreglem2  23245  kqnrmlem1  23246  kqnrmlem2  23247  hmeoimaf1o  23273  reghmph  23296  nrmhmph  23297  txhmeo  23306  ptuncnv  23310  filconn  23386  fbasrn  23387  fmfnfmlem2  23458  flimfnfcls  23531  cnpfcfi  23543  alexsublem  23547  alexsubALTlem2  23551  alexsubALTlem3  23552  alexsubALTlem4  23553  alexsubALT  23554  ptcmplem3  23557  cnextfval  23565  tsmsxp  23658  imasdsf1olem  23878  bl2in  23905  blssps  23929  blss  23930  blssexps  23931  blssex  23932  blcld  24013  stdbdxmet  24023  met1stc  24029  prdsxmslem2  24037  metcnp3  24048  metcnpi3  24054  txmetcnp  24055  nmo0  24251  nmoid  24258  icccmplem1  24337  icccmp  24340  xrge0tsms  24349  metdseq0  24369  cnheiborlem  24469  cnheibor  24470  cnllycmp  24471  pcoval2  24531  cmetcaulem  24804  iscmet3lem1  24807  iscmet3lem2  24808  equivcau  24816  lmcau  24829  cncmet  24838  ivthlem2  24968  ivthlem3  24969  ovoliunlem2  25019  ovolscalem2  25030  uniioombl  25105  dyaddisj  25112  opnmbllem  25117  volivth  25123  ismbfd  25155  ismbf3d  25170  mbfimaopnlem  25171  mbfinf  25181  itg1addlem4  25215  itg1addlem4OLD  25216  mbfi1fseqlem1  25232  mbfi1fseqlem3  25234  mbfi1fseqlem4  25235  mbfi1fseqlem5  25236  mbfi1fseqlem6  25237  itg2seq  25259  itg2lea  25261  itg2split  25266  itg2cnlem1  25278  bddiblnc  25358  limciun  25410  dvmptfsum  25491  rolle  25506  c1lip1  25513  dvcnvrelem1  25533  dvcnvre  25535  dvcvx  25536  itgsubst  25565  tdeglem4  25576  tdeglem4OLD  25577  mdegmullem  25595  plyco0  25705  coemullem  25763  dgreq0  25778  dgrmul  25783  dgrco  25788  elqaalem2  25832  aannenlem1  25840  aaliou3lem9  25862  ulmres  25899  ulmshftlem  25900  angneg  26305  dcubic  26348  cxploglim  26479  cxploglim2  26480  scvxcvx  26487  lgamgulmlem5  26534  lgamcvg2  26556  ftalem2  26575  basellem3  26584  basellem4  26585  sqff1o  26683  fsumdvdsdiaglem  26684  dvdsflsumcom  26689  dvdsmulf1o  26695  fsumvma2  26714  logfac2  26717  logfacrlim  26724  logexprlim  26725  dchrelbasd  26739  lgsne0  26835  lgsqrlem2  26847  lgsqrmodndvds  26853  gausslemma2dlem1a  26865  lgseisenlem2  26876  lgsquadlem1  26880  lgsquadlem2  26881  lgsquadlem3  26882  lgsquad2lem2  26885  2sqlem8  26926  2sqlem11  26929  2sqreultlem  26947  2sqreunnltlem  26950  chpo1ubb  26981  vmadivsum  26982  rplogsumlem2  26985  rpvmasumlem  26987  dchrmusum2  26994  dchrvmasumlem1  26995  dchrisum0fno1  27011  dchrisum0re  27013  dchrisum0lem1  27016  dchrisum0lem2  27018  dchrisum0lem3  27019  dchrisum0  27020  mulogsumlem  27031  mulog2sumlem2  27035  vmalogdivsum2  27038  logsqvma  27042  log2sumbnd  27044  selberglem3  27047  selberg  27048  selberg2lem  27050  selberg2b  27052  selberg3lem2  27058  pntrmax  27064  pntrsumo1  27065  pntlemn  27100  pntlemp  27110  qabvle  27125  ostthlem1  27127  ostthlem2  27128  ostth2lem2  27134  ostth3  27138  sltres  27162  nosupno  27203  nosupbnd2  27216  noinfno  27218  noinfbnd2  27231  etasslt  27311  cuteq1  27331  addsproplem2  27451  mulsval  27562  precsexlem11  27660  idmot  27785  brbtwn2  28160  colinearalglem4  28164  colinearalg  28165  ax5seglem9  28192  axpaschlem  28195  axcontlem2  28220  axcontlem7  28225  axcontlem8  28226  eengtrkg  28241  upgr1eopALT  28374  uspgredg2vlem  28477  subumgr  28542  nbgr0vtxlem  28609  edgnbusgreu  28621  nb3grprlem1  28634  wlkl1loop  28892  pthdivtx  28983  usgr2pth  29018  crctcshwlkn0  29072  wlklnwwlkln1  29119  wwlksnext  29144  clwwlkccatlem  29239  clwlkclwwlklem2a  29248  clwwlkinwwlk  29290  clwwlkn1loopb  29293  clwwlkf  29297  wwlksext2clwwlk  29307  wwlksubclwwlk  29308  clwwlknscsh  29312  clwwlknon1  29347  clwwlknonex2e  29360  1conngr  29444  n4cyclfrgr  29541  numclwwlk2lem1lem  29592  2clwwlk2clwwlk  29600  numclwwlk1lem2f1  29607  numclwlk1lem1  29619  numclwwlk2lem1  29626  numclwlk2lem2f  29627  numclwwlk7  29641  frgrogt3nreg  29647  grpoidinvlem1  29752  grpoidinvlem3  29754  grporcan  29766  nmlnoubi  30044  blocnilem  30052  ipblnfi  30103  htthlem  30165  ocsh  30531  shmodsi  30637  pjhthlem2  30640  5oalem2  30903  eigposi  31084  nmopub2tALT  31157  nmfnleub2  31174  nmcexi  31274  nmopcoi  31343  kbass3  31366  mdslmd1lem1  31573  mdslmd1lem2  31574  chirredlem2  31639  chirredlem4  31641  mdsymlem3  31653  mdsymlem5  31655  sumdmdii  31663  sumdmdlem  31666  sumdmdlem2  31667  foresf1o  31737  disjxpin  31814  1stpreimas  31922  resf1o  31950  nn0xmulclb  31979  wrdt2ind  32112  xrge0tsmsd  32204  gsumvsca1  32366  gsumvsca2  32367  islinds5  32475  irngnzply1  32750  mdetpmtr1  32798  mdetpmtr2  32799  pstmxmet  32872  qqhghm  32963  qqhrhm  32964  esumpcvgval  33071  volmeas  33224  imambfm  33256  dya2iocnrect  33275  oddpwdc  33348  sseqf  33386  orvcgteel  33461  orvclteel  33466  ballotlemsf1o  33507  bnj1110  33988  bnj1118  33990  f1resveqaeq  34083  txpconn  34218  connpconn  34221  cnllysconn  34231  rellysconn  34237  cvmsss2  34260  cvmlift2lem9  34297  satf00  34360  fmlasuc  34372  mrsubfval  34494  mppsval  34558  dfon2lem6  34755  wzel  34791  ifscgr  35011  cgrxfr  35022  btwnconn1lem5  35058  btwnconn1lem6  35059  btwnconn1lem12  35065  brsegle  35075  finminlem  35198  nn0prpwlem  35202  fnessref  35237  refssfne  35238  neibastop1  35239  topjoin  35245  fnemeet2  35247  bj-prmoore  35991  bj-finsumval0  36161  topdifinffinlem  36223  lindsadd  36476  matunitlindflem2  36480  poimirlem28  36511  poimirlem32  36515  opnmbllem0  36519  mblfinlem1  36520  mblfinlem4  36523  ismblfin  36524  mbfresfi  36529  itg2addnclem  36534  itg2addnclem3  36536  itg2addnc  36537  unirep  36577  frinfm  36598  sdclem2  36605  geomcau  36622  istotbnd3  36634  sstotbnd2  36637  sstotbnd  36638  sstotbnd3  36639  totbndbnd  36652  cntotbnd  36659  ismtyres  36671  heibor1lem  36672  heiborlem1  36674  heiborlem8  36681  ismndo1  36736  isdivrngo  36813  unichnidl  36894  erimeq2  37543  cvlcvr1  38204  ishlat3N  38219  llnmlplnN  38405  islvol2aN  38458  4atlem4c  38467  4atlem4d  38468  isline2  38640  isline3  38642  linepsubclN  38817  lhpexle3lem  38877  lhpjat2  38887  cdlemd4  39067  cdleme0cq  39081  cdleme32fva  39303  cdleme32fvaw  39305  tendo0mul  39692  tendo0mulr  39693  diameetN  39922  dvhvaddcl  39961  dvhvaddcomN  39962  cdlemm10N  39984  dvadiaN  39994  djavalN  40001  dihvalcqat  40105  dihopelvalcpre  40114  djhval  40264  dihjat1lem  40294  sticksstones11  40967  sticksstones22  40979  metakunt15  40994  metakunt16  40995  f1o2d2  41057  evlselvlem  41160  evlselv  41161  fsuppind  41164  mhpind  41168  remul01  41281  zaddcom  41326  zmulcom  41330  prjspertr  41348  prjsprellsp  41354  elrfi  41422  nacsfix  41440  fzsplit1nn0  41482  eldioph2  41490  lzenom  41498  irrapxlem3  41552  pellexlem5  41561  pell1234qrne0  41581  pell1234qrmulcl  41583  pell14qrdich  41597  pell1qrge1  41598  pellqrex  41607  reglogltb  41619  reglogleb  41620  rmxypairf1o  41640  rmxycomplete  41646  monotoddzzfi  41671  congadd  41695  congsym  41697  acongrep  41709  jm2.19lem3  41720  jm2.19lem4  41721  jm2.22  41724  jm2.25  41728  expdiophlem1  41750  wepwsolem  41774  kelac1  41795  lmhmfgsplit  41818  pwslnm  41826  hbtlem6  41861  hbt  41862  mon1psubm  41938  deg1mhm  41939  omord2lim  42040  succlg  42068  onmcl  42071  ofoafo  42096  ofoacom  42101  fzunt  42196  fzuntd  42197  fzunt1d  42198  fzuntgd  42199  iunrelexp0  42443  dssmapnvod  42761  gsumws3  42938  gsumws4  42939  mulltgt0  43696  fnchoice  43703  disjrnmpt2  43876  fzisoeu  44000  fsumiunss  44281  climinf  44312  mullimc  44322  mullimcf  44329  stoweidlem14  44720  stoweidlem17  44723  stoweidlem34  44740  stoweidlem50  44756  fourierdlem42  44855  fourierdlem62  44874  fourierdlem71  44883  fourierdlem76  44888  qndenserrnbllem  45000  subsaliuncl  45064  sge0resplit  45112  upwrdfi  45591  2reu8i  45811  fundcmpsurinjpreimafv  46066  iccpartigtl  46081  prproropf1olem2  46162  prproropf1olem4  46164  paireqne  46169  prmdvdsfmtnof1lem2  46243  bgoldbtbndlem3  46465  bgoldbtbnd  46467  isomushgr  46484  isomuspgrlem2c  46488  uspgrsprf1  46515  subsubmgm  46557  isassintop  46610  subsubrng  46732  2zlidl  46822  2zrngnmrid  46838  rngcinv  46869  rngcinvALTV  46881  ringcinv  46920  funcringcsetcALTV2lem9  46932  ringcinvALTV  46944  funcringcsetclem9ALTV  46955  fldhmsubc  46972  fldhmsubcALTV  46990  mndpsuppss  47037  gsumlsscl  47049  lincsum  47100  lindslinindsimp1  47128  lindslinindimp2lem4  47132  lincresunitlem2  47147  elfzolborelfzop1  47190  elbigo2  47228  digexp  47283  dig1  47284  nn0sumshdiglemB  47296  1arymaptf1  47318  2arymaptf1  47329  itcoval1  47339  itcoval2  47340  itcoval3  47341  itcovalsucov  47344  ackvalsuc1mpt  47354  itschlc0xyqsol  47443  thincciso  47659  indthinc  47662  indthincALT  47663