Theorem ad2antrl 760

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	adantr 480	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜓)
3	2	adantl 481	1 ⊢ ((𝜒 ∧ (𝜑 ∧ 𝜃)) → 𝜓)

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  simprl  790  simprll  798  simprlr  799  disjxiun  4579  reusv2lem4  4798  fr2nr  5016  somin1  5448  tz7.7  5666  f1oprg  6093  soisores  6477  elovmpt2rab1  6779  sorpssi  6841  onint  6887  ordsucelsuc  6914  elxp5  7004  wemoiso  7044  wemoiso2  7045  el2xptp0  7103  ressuppss  7201  imacosupp  7222  tz7.48lem  7423  oalimcl  7527  oeeui  7569  oaabs2  7612  omabs  7614  swoer  7659  0erOLD  7668  ralxpmap  7793  pw2f1olem  7949  enfixsn  7954  mapxpen  8011  mapunen  8014  unxpdomlem2  8050  unxpdomlem3  8051  findcard3  8088  isfinite2  8103  domunfican  8118  fodomfi  8124  fissuni  8154  fipreima  8155  indexfi  8157  fsuppsssupp  8174  marypha1lem  8222  marypha2  8228  supmo  8241  infmo  8284  oieu  8327  brwdom2  8361  ixpiunwdom  8379  cantnfval2  8449  cantnfle  8451  cantnflt  8452  cantnf  8473  wemapwe  8477  cnfcom  8480  rankonidlem  8574  r1pwcl  8593  infxpenlem  8719  infxpenc2lem1  8725  fseqenlem1  8730  dfac8clem  8738  mappwen  8818  dfac3  8827  dfac5  8834  dfac12lem3  8850  cdainf  8897  infunsdom  8919  coftr  8978  ssfin4  9015  domfin4  9016  fin23lem26  9030  fin23lem22  9032  fin23lem28  9045  fin23lem32  9049  fin23lem40  9056  isf32lem5  9062  compssiso  9079  isf34lem4  9082  isfin1-3  9091  fin1a2lem13  9117  hsmexlem2  9132  hsmexlem4  9134  zorn2lem1  9201  ttukeylem6  9219  iundom2g  9241  konigthlem  9269  pwcfsdom  9284  fpwwe2lem12  9342  fpwwe2  9344  pwfseqlem3  9361  winalim2  9397  r1wunlim  9438  inttsk  9475  inar1  9476  grur1  9521  nqereq  9636  ltexprlem7  9743  prlem936  9748  00id  10090  addid2  10098  ltord1  10433  divdiv1  10615  divdiv2  10616  conjmul  10621  ltdivmul  10777  ledivmul  10778  lt2mul2div  10780  ltdiv23  10793  lediv23  10794  lediv12a  10795  ledivp1  10804  negfi  10850  nn0nndivcl  11239  nn0ge0div  11322  peano2uz2  11341  peano5uzi  11342  eluzp1m1  11587  qbtwnre  11904  xralrple  11910  xleadd1a  11955  xmulge0  11986  xmulass  11989  xlemul1a  11990  iooshf  12123  divelunit  12185  eluzgtdifelfzo  12397  modadd1  12569  modmul1  12585  seqcl2  12681  seqfveq2  12685  seqid2  12709  seqhomo  12710  seqdistr  12714  mulexpz  12762  leexp2r  12780  expnlbnd2  12857  expmulnbnd  12858  hashmap  13082  hashfun  13084  hashbclem  13093  hashfacen  13095  hashf1lem2  13097  hashf1  13098  ccatsymb  13219  swrdsb0eq  13299  swrdswrd  13312  wrdind  13328  wrd2ind  13329  swrdccatin1  13334  swrdccatin2  13338  swrdccatin12  13342  swrdccat  13344  splid  13355  repswswrd  13382  0csh0  13390  2cshw  13410  cshweqrep  13418  relexp0g  13610  relexpsucnnr  13613  relexpindlem  13651  sqrlem1  13831  sqrlem6  13836  rlim  14074  rlimclim1  14124  climsup  14248  caurcvg2  14256  caucvgb  14258  iseralt  14263  sumss  14302  fsum2dlem  14343  mptfzshft  14352  modfsummod  14367  o1fsum  14386  incexclem  14407  divrcnv  14423  flo1  14425  fprodrev  14546  fprod2dlem  14549  ruclem6  14803  moddvds  14829  dvdsaddre2b  14867  dvdsflip  14877  addmodlteqALT  14885  fldivndvdslt  14976  bitsf1ocnv  15004  bitsf1  15006  sadcaddlem  15017  bezoutlem2  15095  bezoutlem4  15097  lcmgcdlem  15157  prmind2  15236  isprm5  15257  isprm6  15264  cncongrprm  15275  hashdvds  15318  crth  15321  eulerthlem2  15325  prmdiveq  15329  hashgcdlem  15331  hashgcdeq  15332  iserodd  15378  pclem  15381  pcprendvds2  15384  pcexp  15402  pcneg  15416  pc2dvds  15421  pcmpt  15434  prmpwdvds  15446  pockthg  15448  prmreclem5  15462  4sqlem11  15497  ramub2  15556  ramubcl  15560  ram0  15564  ramub1lem2  15569  ramcl  15571  prmgaplem3  15595  prmgaplem6  15598  setscom  15731  sscpwex  16298  initoeu2  16489  setcinv  16563  funcestrcsetclem9  16611  funcsetcestrclem9  16626  fullsetcestrc  16629  1stfcl  16660  2ndfcl  16661  hofpropd  16730  isacs3lem  16989  isacs4lem  16991  acsmap2d  17002  submnd0  17143  subsubm  17180  frmdup1  17224  frmdup3lem  17226  sgrp2nmndlem2  17234  isgrpinv  17295  subsubg  17440  cycsubgcl  17443  conjghm  17514  qusghm  17520  gsumwrev  17619  symgfixelsi  17678  symgsssg  17710  symgfisg  17711  psgnunilem2  17738  odf1o2  17811  sylow1lem1  17836  odcau  17842  pgpfi  17843  pgpssslw  17852  fislw  17863  efgtlen  17962  efginvrel2  17963  efgrelexlemb  17986  efgredeu  17988  efgcpbllemb  17991  frgpup1  18011  cygabl  18115  lt6abl  18119  gsum2d  18194  gsum2d2lem  18195  gsum2d2  18196  telgsumfzslem  18208  dmdprdsplit2lem  18267  ablfacrp  18288  pgpfac1lem3  18299  gsummgp0  18431  irredrmul  18530  subsubrg  18629  islss4  18783  lspextmo  18877  lspsnat  18966  issubassa  19145  resspsradd  19237  resspsrmul  19238  coe1tmmul2  19467  pf1ind  19540  prmirredlem  19660  znf1o  19719  znidomb  19729  frgpcyg  19741  psgnghm  19745  psgndiflemB  19765  frlmlbs  19955  frlmup1  19956  lindfind  19974  islindf3  19984  lindfmm  19985  mamulid  20066  mat1dimelbas  20096  mdetdiaglem  20223  mdetralt2  20234  mndifsplit  20261  smadiadetglem2  20297  1elcpmat  20339  pmatcollpw3lem  20407  chfacfisf  20478  chfacfisfcpmat  20479  chfacffsupp  20480  chfacfscmulfsupp  20483  chfacfscmulgsum  20484  chfacfpmmulfsupp  20487  chfacfpmmulgsum  20488  cayhamlem1  20490  cpmadugsumlemF  20500  cayleyhamilton1  20516  tgcl  20584  pptbas  20622  clsval2  20664  mretopd  20706  lmbr2  20873  cncls2  20887  nrmsep  20971  regsep2  20990  cmpsublem  21012  cmpsub  21013  tgcmp  21014  uncmp  21016  hauscmplem  21019  iunconlem  21040  1stcrest  21066  2ndcctbss  21068  2ndcsep  21072  dis2ndc  21073  hausllycmp  21107  dislly  21110  kgentopon  21151  1stckgen  21167  kgencn3  21171  ptpjpre1  21184  ptbasin  21190  ptpjopn  21225  dfac14  21231  ptcnplem  21234  txcn  21239  txindis  21247  txdis1cn  21248  ptrescn  21252  txcmplem1  21254  txcmp  21256  txhaus  21260  txlm  21261  tx1stc  21263  txkgen  21265  xkococn  21273  qtopcn  21327  kqreglem1  21354  kqreglem2  21355  kqnrmlem1  21356  kqnrmlem2  21357  hmeoimaf1o  21383  reghmph  21406  nrmhmph  21407  txhmeo  21416  ptuncnv  21420  filcon  21497  fbasrn  21498  fmfnfmlem2  21569  flimfnfcls  21642  cnpfcfi  21654  alexsublem  21658  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  ptcmplem3  21668  cnextfval  21676  tsmsxp  21768  imasdsf1olem  21988  bl2in  22015  blssps  22039  blss  22040  blssexps  22041  blssex  22042  blcld  22120  stdbdxmet  22130  met1stc  22136  prdsxmslem2  22144  metcnp3  22155  metcnpi3  22161  txmetcnp  22162  nmo0  22349  nmoid  22356  icccmplem1  22433  icccmp  22436  xrge0tsms  22445  metdseq0  22465  cnheiborlem  22561  cnheibor  22562  cnllycmp  22563  pcoval2  22624  cmetcaulem  22894  iscmet3lem1  22897  iscmet3lem2  22898  equivcau  22906  lmcau  22919  cncmet  22927  ivthlem2  23028  ivthlem3  23029  ovoliunlem2  23078  ovolscalem2  23089  uniioombl  23163  dyaddisj  23170  opnmbllem  23175  volivth  23181  ismbfd  23213  ismbf3d  23227  mbfimaopnlem  23228  mbfinf  23238  itg1addlem4  23272  mbfi1fseqlem1  23288  mbfi1fseqlem3  23290  mbfi1fseqlem4  23291  mbfi1fseqlem5  23292  mbfi1fseqlem6  23293  itg2seq  23315  itg2lea  23317  itg2split  23322  itg2cnlem1  23334  limciun  23464  dvmptfsum  23542  rolle  23557  c1lip1  23564  dvcnvrelem1  23584  dvcnvre  23586  dvcvx  23587  itgsubst  23616  tdeglem4  23624  mdegmullem  23642  plyco0  23752  coemullem  23810  dgreq0  23825  dgrmul  23830  dgrco  23835  elqaalem2  23879  aannenlem1  23887  aaliou3lem9  23909  ulmres  23946  ulmshftlem  23947  angneg  24333  dcubic  24373  cxploglim  24504  cxploglim2  24505  scvxcvx  24512  lgamgulmlem5  24559  lgamcvg2  24581  basellem3  24609  basellem4  24610  sqff1o  24708  fsumdvdsdiaglem  24709  dvdsflsumcom  24714  dvdsmulf1o  24720  fsumvma2  24739  logfac2  24742  logfacrlim  24749  logexprlim  24750  dchrelbasd  24764  lgsne0  24860  lgsqrlem2  24872  lgsqrmodndvds  24878  gausslemma2dlem1a  24890  lgseisenlem2  24901  lgsquadlem1  24905  lgsquadlem2  24906  lgsquadlem3  24907  lgsquad2lem2  24910  2sqlem8  24951  2sqlem11  24954  chpo1ubb  24970  vmadivsum  24971  rplogsumlem2  24974  rpvmasumlem  24976  dchrmusum2  24983  dchrvmasumlem1  24984  dchrisum0fno1  25000  dchrisum0re  25002  dchrisum0lem1  25005  dchrisum0lem2  25007  dchrisum0lem3  25008  dchrisum0  25009  mulogsumlem  25020  mulog2sumlem2  25024  vmalogdivsum2  25027  logsqvma  25031  log2sumbnd  25033  selberglem3  25036  selberg  25037  selberg2lem  25039  selberg2b  25041  selberg3lem2  25047  pntrmax  25053  pntrsumo1  25054  pntlemn  25089  pntlemp  25099  qabvle  25114  ostthlem1  25116  ostthlem2  25117  ostth2lem2  25123  ostth3  25127  idmot  25232  iscgra1  25502  brbtwn2  25585  colinearalglem4  25589  colinearalg  25590  ax5seglem9  25617  axpaschlem  25620  axcontlem2  25645  axcontlem7  25650  axcontlem8  25651  eengtrkg  25665  upgr1eopALT  25783  umgra1  25855  uslgra1  25901  nb3graprlem1  25980  nbcusgra  25992  uvtxnbgravtx  26023  wlkntrllem3  26091  vfwlkniswwlkn  26234  wwlknext  26252  clwlkisclwwlklem2a  26313  clwwlkf  26322  clwwlknscsh  26347  clwlkfoclwwlk  26372  vdgrf  26425  iseupa  26492  eupai  26494  n4cyclfrgra  26545  frgrawopreg  26576  2spotdisj  26588  clwwlkextfrlem1  26603  extwwlkfablem2  26605  numclwwlkovf2ex  26613  numclwlk1lem2f1  26621  numclwwlk2lem1  26629  numclwlk2lem2f  26630  numclwwlk6  26640  numclwwlk7  26641  frgraogt3nreg  26647  grpoidinvlem1  26742  grpoidinvlem3  26744  grporcan  26756  nmlnoubi  27035  blocnilem  27043  ipblnfi  27095  htthlem  27158  ocsh  27526  shmodsi  27632  pjhthlem2  27635  5oalem2  27898  eigposi  28079  nmopub2tALT  28152  nmfnleub2  28169  nmcexi  28269  nmopcoi  28338  kbass3  28361  mdslmd1lem1  28568  mdslmd1lem2  28569  chirredlem2  28634  chirredlem4  28636  mdsymlem3  28648  mdsymlem5  28650  sumdmdii  28658  sumdmdlem  28661  sumdmdlem2  28662  foresf1o  28727  disjxpin  28783  1stpreimas  28866  resf1o  28893  gsumvsca1  29113  gsumvsca2  29114  xrge0tsmsd  29116  mdetpmtr1  29217  mdetpmtr2  29218  pstmxmet  29268  qqhghm  29360  qqhrhm  29361  esumpcvgval  29467  volmeas  29621  imambfm  29651  dya2iocnrect  29670  oddpwdc  29743  sseqf  29781  orvcgteel  29856  orvclteel  29861  ballotlemsf1o  29902  bnj1110  30304  bnj1118  30306  txpcon  30468  conpcon  30471  cnllyscon  30481  rellyscon  30487  cvmsss2  30510  cvmlift2lem9  30547  mrsubfval  30659  mppsval  30723  dfon2lem6  30937  trpredmintr  30975  wzel  31015  wzelOLD  31016  sltres  31061  ifscgr  31321  cgrxfr  31332  btwnconn1lem5  31368  btwnconn1lem6  31369  btwnconn1lem12  31375  brsegle  31385  finminlem  31482  gtinfOLD  31484  nn0prpwlem  31487  fnessref  31522  refssfne  31523  neibastop1  31524  topjoin  31530  fnemeet2  31532  bj-finsumval0  32324  topdifinffinlem  32371  matunitlindflem2  32576  poimirlem28  32607  poimirlem32  32611  opnmbllem0  32615  mblfinlem1  32616  mblfinlem4  32619  ismblfin  32620  mbfresfi  32626  itg2addnclem  32631  itg2addnclem3  32633  itg2addnc  32634  bddiblnc  32650  unirep  32677  frinfm  32700  sdclem2  32708  geomcau  32725  istotbnd3  32740  sstotbnd2  32743  sstotbnd  32744  sstotbnd3  32745  totbndbnd  32758  cntotbnd  32765  ismtyres  32777  heibor1lem  32778  heiborlem1  32780  heiborlem8  32787  ismndo1  32842  isdivrngo  32919  unichnidl  33000  cvlcvr1  33644  ishlat3N  33659  llnmlplnN  33843  islvol2aN  33896  4atlem4c  33905  4atlem4d  33906  isline2  34078  isline3  34080  linepsubclN  34255  lhpexle3lem  34315  lhpjat2  34325  cdlemd4  34506  cdleme0cq  34520  cdleme32fva  34743  cdleme32fvaw  34745  tendo0mul  35132  tendo0mulr  35133  diameetN  35363  dvhvaddcl  35402  dvhvaddcomN  35403  cdlemm10N  35425  dvadiaN  35435  djavalN  35442  dihvalcqat  35546  dihopelvalcpre  35555  djhval  35705  dihjat1lem  35735  elrfi  36275  nacsfix  36293  fzsplit1nn0  36335  eldioph2  36343  lzenom  36351  irrapxlem3  36406  pellexlem5  36415  pell1234qrne0  36435  pell1234qrmulcl  36437  pell14qrdich  36451  pell1qrge1  36452  pellqrex  36461  reglogltb  36473  reglogleb  36474  rmxypairf1o  36494  rmxycomplete  36500  monotoddzzfi  36525  congadd  36551  congsym  36553  acongrep  36565  jm2.19lem3  36576  jm2.19lem4  36577  jm2.22  36580  jm2.25  36584  expdiophlem1  36606  wepwsolem  36630  kelac1  36651  lmhmfgsplit  36674  pwslnm  36682  hbtlem6  36718  hbt  36719  mon1psubm  36803  deg1mhm  36804  iunrelexp0  37013  dssmapnvod  37334  gsumws3  37521  gsumws4  37522  mulltgt0  38204  fnchoice  38211  disjrnmpt2  38370  fzisoeu  38455  fsumiunss  38642  climinf  38673  mullimc  38683  mullimcf  38690  stoweidlem14  38907  stoweidlem17  38910  stoweidlem34  38927  stoweidlem50  38943  fourierdlem42  39042  fourierdlem62  39061  fourierdlem71  39070  fourierdlem76  39075  qndenserrnbllem  39190  subsaliuncl  39252  sge0resplit  39299  iccpartigtl  39961  prmdvdsfmtnof1lem2  40035  bgoldbtbndlem3  40223  bgoldbtbnd  40225  ccatpfx  40272  pfxccatin12lem2  40287  pfxccatin12  40288  uspgredg2vlem  40450  subumgr  40512  edgnbusgreu  40595  nb3grprlem1  40608  1wlkl1loop  40842  pthdivtx  40935  usgr2pth  40970  crctcsh1wlkn0  41024  1wlklnwwlkln1  41065  wwlksnext  41099  clwlkclwwlklem2a  41207  clwwlksf  41222  wwlksubclwwlks  41232  clwwnisshclwwsn  41237  clwwlksnscsh  41247  1conngr  41361  n4cyclfrgr  41461  frgrwopreg  41486  frgrhash2wsp  41497  av-numclwwlkovf2ex  41517  av-numclwlk1lem2f1  41524  av-numclwwlk2lem1  41532  av-numclwlk2lem2f  41533  av-numclwwlk7  41545  av-frgraogt3nreg  41551  subsubmgm  41587  isassintop  41636  2zlidl  41724  2zrngnmrid  41740  rngcinv  41773  rngcinvALTV  41785  ringcinv  41824  funcringcsetcALTV2lem9  41836  ringcinvALTV  41848  funcringcsetclem9ALTV  41859  fldhmsubc  41876  fldhmsubcALTV  41895  mndpsuppss  41946  gsumlsscl  41958  lincsum  42012  lindslinindsimp1  42040  lindslinindimp2lem4  42044  lincresunitlem2  42059  elfzolborelfzop1  42103  elbigo2  42144  digexp  42199  dig1  42200  nn0sumshdiglemB  42212