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  770  simprll  778  simprlr  779  simprl1  1219  simprl2  1220  simprl3  1221  disjxiun  5104  reusv2lem4  5356  axprlem5OLD  5385  fr2nr  5615  somin1  6106  tz7.7  6358  f1oprg  6845  soisores  7302  elovmporab1w  7636  elovmporab1  7637  sorpssi  7705  onint  7766  ordsucelsuc  7797  elxp5  7899  resf1extb  7910  f1oabexg  7918  wemoiso  7952  wemoiso2  7953  el2xptp0  8015  frxp2  8123  frxp3  8130  ressuppss  8162  fprlem1  8279  tz7.48lem  8409  oalimcl  8524  oeeui  8566  nnaordex2  8603  oaabs2  8613  omabs  8615  swoer  8702  ralxpmap  8869  pw2f1olem  9045  enfixsn  9050  mapxpen  9107  mapunen  9110  php  9171  unxpdomlem2  9198  unxpdomlem3  9199  findcard3OLD  9230  isfinite2  9245  fodomfi  9261  domunfican  9272  fodomfiOLD  9281  fissuni  9308  fipreima  9309  indexfi  9311  fsuppsssupp  9332  marypha1lem  9384  marypha2  9390  supmo  9403  infmo  9448  oieu  9492  brwdom2  9526  ixpiunwdom  9543  cantnfval2  9622  cantnfle  9624  cantnflt  9625  cantnf  9646  wemapwe  9650  cnfcom  9653  frrlem15  9710  rankonidlem  9781  r1pwcl  9800  eldju2ndl  9877  eldju2ndr  9878  djuun  9879  infxpenlem  9966  infxpenc2lem1  9972  fseqenlem1  9977  dfac8clem  9985  mappwen  10065  dfac3  10074  dfac5  10082  dfac12lem3  10099  infunsdom  10166  coftr  10226  ssfin4  10263  domfin4  10264  fin23lem26  10278  fin23lem22  10280  fin23lem28  10293  fin23lem32  10297  fin23lem40  10304  isf32lem5  10310  compssiso  10327  isf34lem4  10330  isfin1-3  10339  fin1a2lem13  10365  hsmexlem2  10380  hsmexlem4  10382  zorn2lem1  10449  ttukeylem6  10467  iundom2g  10493  konigthlem  10521  pwcfsdom  10536  fpwwe2lem11  10594  fpwwe2  10596  pwfseqlem3  10613  winalim2  10649  r1wunlim  10690  inttsk  10727  inar1  10728  grur1  10773  nqereq  10888  ltexprlem7  10995  prlem936  11000  00id  11349  addlid  11357  ltord1  11704  divdiv1  11893  divdiv2  11894  conjmul  11899  ltdivmul  12058  ledivmul  12059  lt2mul2div  12061  ltdiv23  12074  lediv23  12075  lediv12a  12076  ledivp1  12085  negfi  12132  nn0nndivcl  12514  nn0ge0div  12603  peano2uz2  12622  peano5uzi  12623  eluzp1m1  12819  qbtwnre  13159  xralrple  13165  xleadd1a  13213  xmulge0  13244  xmulass  13247  xlemul1a  13248  iooshf  13387  divelunit  13455  eluzgtdifelfzo  13688  modadd1  13870  modmul1  13889  seqcl2  13985  seqfveq2  13989  seqid2  14013  seqhomo  14014  seqdistr  14018  mulexpz  14067  leexp2r  14139  expnlbnd2  14199  expmulnbnd  14200  hashmap  14400  hashfun  14402  hashbclem  14417  hashfacen  14419  hashf1lem2  14421  hashf1  14422  ccatsymb  14547  swrdwrdsymb  14627  swrdsb0eq  14628  ccatpfx  14666  swrdswrd  14670  wrdind  14687  wrd2ind  14688  swrdccatin1  14690  swrdccatin2  14694  pfxccatin12lem2  14696  pfxccatin12  14698  swrdccat  14700  repswswrd  14749  0csh0  14758  cshwidxmod  14768  2cshw  14778  cshweqrep  14786  relexp0g  14988  relexpsucnnr  14991  relexpindlem  15029  01sqrexlem1  15208  01sqrexlem6  15213  rlim  15461  rlimclim1  15511  climsup  15636  caurcvg2  15644  caucvgb  15646  iseralt  15651  sumss  15690  fsum2dlem  15736  mptfzshft  15744  modfsummod  15760  o1fsum  15779  incexclem  15802  divrcnv  15818  flo1  15820  fprodrev  15943  fprod2dlem  15946  ruclem6  16203  moddvds  16233  dvdsaddre2b  16277  dvdsflip  16287  addmodlteqALT  16295  nn0o  16353  fldivndvdslt  16386  bitsf1ocnv  16414  bitsf1  16416  sadcaddlem  16427  bezoutlem2  16510  bezoutlem4  16512  lcmgcdlem  16576  prmind2  16655  isprm5  16677  isprm6  16684  prmdvdsncoprmbd  16697  cncongrprm  16699  hashdvds  16745  crth  16748  eulerthlem2  16752  prmdiveq  16756  hashgcdlem  16758  hashgcdeq  16760  iserodd  16806  pclem  16809  pcprendvds2  16812  pcexp  16830  pcneg  16845  pc2dvds  16850  pcmpt  16863  prmpwdvds  16875  pockthg  16877  prmreclem5  16891  4sqlem11  16926  ramub2  16985  ramubcl  16989  ram0  16993  ramub1lem2  16998  ramcl  17000  prmgaplem3  17024  prmgaplem6  17027  setscom  17150  sscpwex  17777  initoeu2  17978  setcinv  18052  funcestrcsetclem9  18109  funcsetcestrclem9  18124  fullsetcestrc  18127  1stfcl  18158  2ndfcl  18159  hofpropd  18228  isacs3lem  18501  isacs4lem  18503  acsmap2d  18514  subsubmgm  18637  submnd0  18690  mndpsuppss  18692  subsubm  18743  insubm  18745  frmdup1  18791  frmdup3lem  18793  sgrp2nmndlem2  18851  isgrpinv  18925  subsubg  19081  cycsubgcl  19138  conjghm  19181  qusghm  19187  gsumwrev  19298  gsmsymgrfixlem1  19357  symgfixelsi  19365  symgsssg  19397  symgfisg  19398  psgnunilem2  19425  odf1o2  19503  sylow1lem1  19528  odcau  19534  pgpfi  19535  pgpssslw  19544  fislw  19555  efgtlen  19656  efginvrel2  19657  efgrelexlemb  19680  efgredeu  19682  efgcpbllemb  19685  frgpup1  19705  lt6abl  19825  gsum2d  19902  gsum2d2lem  19903  gsum2d2  19904  telgsumfzslem  19918  dmdprdsplit2lem  19977  ablfacrp  19998  pgpfac1lem3  20009  gsummgp0  20227  irredrmul  20336  subsubrng  20472  subsubrg  20507  rngcinv  20546  ringcinv  20580  fldhmsubc  20694  islss4  20868  lspextmo  20963  lspsnat  21055  prmirredlem  21382  znf1o  21461  znidomb  21471  frgpcyg  21483  psgnghm  21489  psgndiflemB  21509  frlmlbs  21706  frlmup1  21707  lindfind  21725  islindf3  21735  lindfmm  21736  issubassa3  21775  resspsradd  21884  resspsrmul  21885  psdmul  22053  coe1tmmul2  22162  pf1ind  22242  mamulid  22328  mat1dimelbas  22358  mdetdiaglem  22485  mdetralt2  22496  mndifsplit  22523  smadiadetglem2  22559  1elcpmat  22602  pmatcollpw3lem  22670  chfacfisf  22741  chfacfisfcpmat  22742  chfacffsupp  22743  chfacfscmulfsupp  22746  chfacfscmulgsum  22747  chfacfpmmulfsupp  22750  chfacfpmmulgsum  22751  chfacfpmmulgsum2  22752  cayhamlem1  22753  cpmadugsumlemF  22763  cayleyhamilton1  22779  tgcl  22856  pptbas  22895  clsval2  22937  mretopd  22979  lmbr2  23146  cncls2  23160  nrmsep  23244  regsep2  23263  cmpsublem  23286  cmpsub  23287  tgcmp  23288  uncmp  23290  hauscmplem  23293  iunconnlem  23314  1stcrest  23340  2ndcctbss  23342  2ndcsep  23346  dis2ndc  23347  hausllycmp  23381  dislly  23384  kgentopon  23425  1stckgen  23441  kgencn3  23445  ptpjpre1  23458  ptbasin  23464  ptpjopn  23499  dfac14  23505  ptcnplem  23508  txcn  23513  txindis  23521  txdis1cn  23522  ptrescn  23526  txcmplem1  23528  txcmp  23530  txhaus  23534  txlm  23535  tx1stc  23537  txkgen  23539  xkococn  23547  qtopcn  23601  kqreglem1  23628  kqreglem2  23629  kqnrmlem1  23630  kqnrmlem2  23631  hmeoimaf1o  23657  reghmph  23680  nrmhmph  23681  txhmeo  23690  ptuncnv  23694  filconn  23770  fbasrn  23771  fmfnfmlem2  23842  flimfnfcls  23915  cnpfcfi  23927  alexsublem  23931  alexsubALTlem2  23935  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  ptcmplem3  23941  cnextfval  23949  tsmsxp  24042  imasdsf1olem  24261  bl2in  24288  blssps  24312  blss  24313  blssexps  24314  blssex  24315  blcld  24393  stdbdxmet  24403  met1stc  24409  prdsxmslem2  24417  metcnp3  24428  metcnpi3  24434  txmetcnp  24435  nmo0  24623  nmoid  24630  icccmplem1  24711  icccmp  24714  xrge0tsms  24723  metdseq0  24743  cnheiborlem  24853  cnheibor  24854  cnllycmp  24855  pcoval2  24916  cmetcaulem  25188  iscmet3lem1  25191  iscmet3lem2  25192  equivcau  25200  lmcau  25213  cncmet  25222  ivthlem2  25353  ivthlem3  25354  ovoliunlem2  25404  ovolscalem2  25415  uniioombl  25490  dyaddisj  25497  opnmbllem  25502  volivth  25508  ismbfd  25540  ismbf3d  25555  mbfimaopnlem  25556  mbfinf  25566  itg1addlem4  25600  mbfi1fseqlem1  25616  mbfi1fseqlem3  25618  mbfi1fseqlem4  25619  mbfi1fseqlem5  25620  mbfi1fseqlem6  25621  itg2seq  25643  itg2lea  25645  itg2split  25650  itg2cnlem1  25662  bddiblnc  25743  limciun  25795  dvmptfsum  25879  rolle  25894  c1lip1  25902  dvcnvrelem1  25922  dvcnvre  25924  dvcvx  25925  itgsubst  25956  tdeglem4  25965  mdegmullem  25983  plyco0  26097  coemullem  26155  dgreq0  26171  dgrmul  26176  dgrco  26181  elqaalem2  26228  aannenlem1  26236  aaliou3lem9  26258  ulmres  26297  ulmshftlem  26298  angneg  26713  dcubic  26756  cxploglim  26888  cxploglim2  26889  scvxcvx  26896  lgamgulmlem5  26943  lgamcvg2  26965  ftalem2  26984  basellem3  26993  basellem4  26994  sqff1o  27092  fsumdvdsdiaglem  27093  dvdsflsumcom  27098  mpodvdsmulf1o  27104  dvdsmulf1o  27106  fsumvma2  27125  logfac2  27128  logfacrlim  27135  logexprlim  27136  dchrelbasd  27150  lgsne0  27246  lgsqrlem2  27258  lgsqrmodndvds  27264  gausslemma2dlem1a  27276  lgseisenlem2  27287  lgsquadlem1  27291  lgsquadlem2  27292  lgsquadlem3  27293  lgsquad2lem2  27296  2sqlem8  27337  2sqlem11  27340  2sqreultlem  27358  2sqreunnltlem  27361  chpo1ubb  27392  vmadivsum  27393  rplogsumlem2  27396  rpvmasumlem  27398  dchrmusum2  27405  dchrvmasumlem1  27406  dchrisum0fno1  27422  dchrisum0re  27424  dchrisum0lem1  27427  dchrisum0lem2  27429  dchrisum0lem3  27430  dchrisum0  27431  mulogsumlem  27442  mulog2sumlem2  27446  vmalogdivsum2  27449  logsqvma  27453  log2sumbnd  27455  selberglem3  27458  selberg  27459  selberg2lem  27461  selberg2b  27463  selberg3lem2  27469  pntrmax  27475  pntrsumo1  27476  pntlemn  27511  pntlemp  27521  qabvle  27536  ostthlem1  27538  ostthlem2  27539  ostth2lem2  27545  ostth3  27549  sltres  27574  nosupno  27615  nosupbnd2  27628  noinfno  27630  noinfbnd2  27643  etasslt  27725  cuteq1  27746  addsproplem2  27877  mulsval  28012  precsexlem11  28119  n0sfincut  28246  zmulscld  28285  idmot  28464  brbtwn2  28832  colinearalglem4  28836  colinearalg  28837  ax5seglem9  28864  axpaschlem  28867  axcontlem2  28892  axcontlem7  28897  axcontlem8  28898  eengtrkg  28913  upgr1eopALT  29044  uspgredg2vlem  29150  subumgr  29215  nbgr0edglem  29283  edgnbusgreu  29294  nb3grprlem1  29307  wlkl1loop  29566  pthdivtx  29657  usgr2pth  29694  crctcshwlkn0  29751  wlklnwwlkln1  29798  wwlksnext  29823  clwwlkccatlem  29918  clwlkclwwlklem2a  29927  clwwlkinwwlk  29969  clwwlkn1loopb  29972  clwwlkf  29976  wwlksext2clwwlk  29986  wwlksubclwwlk  29987  clwwlknscsh  29991  clwwlknon1  30026  clwwlknonex2e  30039  1conngr  30123  n4cyclfrgr  30220  numclwwlk2lem1lem  30271  2clwwlk2clwwlk  30279  numclwwlk1lem2f1  30286  numclwlk1lem1  30298  numclwwlk2lem1  30305  numclwlk2lem2f  30306  numclwwlk7  30320  frgrogt3nreg  30326  grpoidinvlem1  30433  grpoidinvlem3  30435  grporcan  30447  nmlnoubi  30725  blocnilem  30733  ipblnfi  30784  htthlem  30846  ocsh  31212  shmodsi  31318  pjhthlem2  31321  5oalem2  31584  eigposi  31765  nmopub2tALT  31838  nmfnleub2  31855  nmcexi  31955  nmopcoi  32024  kbass3  32047  mdslmd1lem1  32254  mdslmd1lem2  32255  chirredlem2  32320  chirredlem4  32322  mdsymlem3  32334  mdsymlem5  32336  sumdmdii  32344  sumdmdlem  32347  sumdmdlem2  32348  foresf1o  32433  disjxpin  32517  1stpreimas  32629  resf1o  32653  nn0xmulclb  32694  wrdt2ind  32875  xrge0tsmsd  33002  gsumvsca1  33179  gsumvsca2  33180  islinds5  33338  1arithidomlem2  33507  irngnzply1  33686  mdetpmtr1  33813  mdetpmtr2  33814  pstmxmet  33887  qqhghm  33978  qqhrhm  33979  esumpcvgval  34068  volmeas  34221  imambfm  34253  dya2iocnrect  34272  oddpwdc  34345  sseqf  34383  orvcgteel  34459  orvclteel  34464  ballotlemsf1o  34505  bnj1110  34972  bnj1118  34974  f1resveqaeq  35075  txpconn  35219  connpconn  35222  cnllysconn  35232  rellysconn  35238  cvmsss2  35261  cvmlift2lem9  35298  satf00  35361  fmlasuc  35373  mrsubfval  35495  mppsval  35559  dfon2lem6  35776  wzel  35812  ifscgr  36032  cgrxfr  36043  btwnconn1lem5  36079  btwnconn1lem6  36080  btwnconn1lem12  36086  brsegle  36096  finminlem  36306  nn0prpwlem  36310  fnessref  36345  refssfne  36346  neibastop1  36347  topjoin  36353  fnemeet2  36355  weiunse  36456  bj-prmoore  37103  bj-finsumval0  37273  topdifinffinlem  37335  lindsadd  37607  matunitlindflem2  37611  poimirlem28  37642  poimirlem32  37646  opnmbllem0  37650  mblfinlem1  37651  mblfinlem4  37654  ismblfin  37655  mbfresfi  37660  itg2addnclem  37665  itg2addnclem3  37667  itg2addnc  37668  unirep  37708  frinfm  37729  sdclem2  37736  geomcau  37753  istotbnd3  37765  sstotbnd2  37768  sstotbnd  37769  sstotbnd3  37770  totbndbnd  37783  cntotbnd  37790  ismtyres  37802  heibor1lem  37803  heiborlem1  37805  heiborlem8  37812  ismndo1  37867  isdivrngo  37944  unichnidl  38025  erimeq2  38670  cvlcvr1  39332  ishlat3N  39347  llnmlplnN  39533  islvol2aN  39586  4atlem4c  39595  4atlem4d  39596  isline2  39768  isline3  39770  linepsubclN  39945  lhpexle3lem  40005  lhpjat2  40015  cdlemd4  40195  cdleme0cq  40209  cdleme32fva  40431  cdleme32fvaw  40433  tendo0mul  40820  tendo0mulr  40821  diameetN  41050  dvhvaddcl  41089  dvhvaddcomN  41090  cdlemm10N  41112  dvadiaN  41122  djavalN  41129  dihvalcqat  41233  dihopelvalcpre  41242  djhval  41392  dihjat1lem  41422  sticksstones11  42144  sticksstones22  42156  f1o2d2  42221  remul01  42395  zaddcom  42452  zmulcom  42456  fidomncyc  42523  evlselvlem  42574  evlselv  42575  fsuppind  42578  mhpind  42582  prjspertr  42593  prjsprellsp  42599  elrfi  42682  nacsfix  42700  fzsplit1nn0  42742  eldioph2  42750  lzenom  42758  irrapxlem3  42812  pellexlem5  42821  pell1234qrne0  42841  pell1234qrmulcl  42843  pell14qrdich  42857  pell1qrge1  42858  pellqrex  42867  reglogltb  42879  reglogleb  42880  rmxypairf1o  42900  rmxycomplete  42906  monotoddzzfi  42931  congadd  42955  congsym  42957  acongrep  42969  jm2.19lem3  42980  jm2.19lem4  42981  jm2.22  42984  jm2.25  42988  expdiophlem1  43010  wepwsolem  43031  kelac1  43052  lmhmfgsplit  43075  pwslnm  43083  hbtlem6  43118  hbt  43119  mon1psubm  43188  deg1mhm  43189  omord2lim  43289  succlg  43317  onmcl  43320  ofoafo  43345  ofoacom  43350  fzunt  43444  fzuntd  43445  fzunt1d  43446  fzuntgd  43447  iunrelexp0  43691  dssmapnvod  44009  gsumws3  44185  gsumws4  44186  mulltgt0  45016  fnchoice  45023  disjrnmpt2  45182  fzisoeu  45298  fsumiunss  45573  climinf  45604  mullimc  45614  mullimcf  45621  stoweidlem14  46012  stoweidlem17  46015  stoweidlem34  46032  stoweidlem50  46048  fourierdlem42  46147  fourierdlem62  46166  fourierdlem71  46175  fourierdlem76  46180  qndenserrnbllem  46292  subsaliuncl  46356  sge0resplit  46404  upwrdfi  46885  3f1oss1  47076  2reu8i  47114  addmodne  47345  fundcmpsurinjpreimafv  47409  iccpartigtl  47424  prproropf1olem2  47505  prproropf1olem4  47507  paireqne  47512  prmdvdsfmtnof1lem2  47586  bgoldbtbndlem3  47808  bgoldbtbnd  47810  grimcnv  47888  gricushgr  47917  cycldlenngric  47928  grimedg  47935  grtrimap  47947  isubgr3stgrlem6  47970  isubgr3stgrlem7  47971  isubgr3stgrlem8  47972  isubgr3stgrlem9  47973  grlimfn  47978  gpgedg2iv  48058  gpg5nbgrvtx03starlem2  48060  gpg5nbgrvtx13starlem2  48063  uspgrsprf1  48135  isassintop  48198  2zlidl  48228  2zrngnmrid  48244  rngcinvALTV  48264  funcringcsetcALTV2lem9  48286  ringcinvALTV  48298  funcringcsetclem9ALTV  48309  fldhmsubcALTV  48321  gsumlsscl  48368  lincsum  48418  lindslinindsimp1  48446  lindslinindimp2lem4  48450  lincresunitlem2  48465  elfzolborelfzop1  48508  elbigo2  48541  digexp  48596  dig1  48597  nn0sumshdiglemB  48609  1arymaptf1  48631  2arymaptf1  48642  itcoval1  48652  itcoval2  48653  itcoval3  48654  itcovalsucov  48657  ackvalsuc1mpt  48667  itschlc0xyqsol  48756  brab2dd  48816  dmrnxp  48825  xpco2  48845  initopropd  49232  termopropd  49233  zeroopropd  49234  prcofpropd  49368  thincciso  49442  indthinc  49451  indthincALT  49452  oduoppcciso  49555  lanpropd  49604  ranpropd  49605