Theorem ad2antrl 741

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  simprl  783  simprll  791  simprlr  792  simprl1  1237  simprl2  1238  simprl3  1239  disjxiun  5103  reusv2lem4  5367  fr2nr  5632  somin1  6133  tz7.7  6395  f1oprg  6882  f1resveqaeq  7287  soisores  7345  elovmporab1w  7678  elovmporab1  7679  sorpssi  7755  onint  7814  ordsucelsuc  7843  elxp5  7945  resf1extb  7956  f1oabexg  7963  wemoiso  7995  wemoiso2  7996  el2xptp0  8057  mpof1o2d  8150  frxp2  8174  frxp3  8181  ressuppss  8214  fprlem1  8332  tz7.48lemOLD  8465  oalimcl  8582  oeeui  8625  nnaordex2  8662  oaabs2  8672  omabs  8674  swoer  8763  ralxpmap  8938  pw2f1olem  9114  enfixsn  9119  mapxpen  9176  mapunen  9179  php  9236  unxpdomlem2  9262  unxpdomlem3  9263  isfinite2  9304  fodomfi  9318  domunfican  9327  fissuni  9360  fipreima  9361  indexfi  9363  fsuppsssupp  9386  marypha1lem  9438  marypha2  9444  supmo  9457  infmo  9502  oieu  9546  brwdom2  9580  ixpiunwdom  9597  cantnfval2  9683  cantnfle  9685  cantnflt  9686  cantnf  9707  wemapwe  9711  cnfcom  9714  frrlem15  9774  rankonidlem  9851  r1pwcl  9874  eldju2ndl  10018  eldju2ndr  10019  djuun  10020  infxpenlem  10105  infxpenc2lem1  10111  fseqenlem1  10116  dfac8clem  10124  mappwen  10204  dfac3  10213  dfac5  10220  dfac12lem3  10237  infunsdom  10304  coftr  10364  ssfin4  10401  domfin4  10402  fin23lem26  10416  fin23lem22  10418  fin23lem28  10431  fin23lem32  10435  fin23lem40  10442  isf32lem5  10448  compssiso  10465  isf34lem4  10468  isfin1-3  10477  fin1a2lem13  10503  hsmexlem2  10518  hsmexlem4  10520  zorn2lem1  10587  ttukeylem6  10605  iundom2g  10637  konigthlem  10666  pwcfsdom  10681  fpwwe2lem11  10739  fpwwe2  10741  pwfseqlem3  10758  winalim2  10794  r1wunlim  10835  inttsk  10872  inar1  10873  grur1  10918  nqereq  11033  ltexprlem7  11140  prlem936  11145  00id  11498  addlid  11506  ltord1  11855  divdiv1  12041  divdiv2  12042  conjmul  12047  ltdivmul  12205  ledivmul  12206  lt2mul2div  12208  ltdiv23  12221  lediv23  12222  lediv12a  12223  ledivp1  12232  negfi  12279  nn0nndivcl  12691  nn0ge0div  12781  peano2uz2  12800  peano5uzi  12801  eluzp1m1  13004  qbtwnre  13342  xralrple  13348  xleadd1a  13396  xmulge0  13427  xmulass  13430  xlemul1a  13431  iooshf  13570  divelunit  13638  eluzgtdifelfzo  13875  modadd1  14061  modmul1  14080  seqcl2  14176  seqfveq2  14180  seqid2  14204  seqhomo  14205  seqdistr  14209  mulexpz  14258  leexp2r  14330  expnlbnd2  14391  expmulnbnd  14392  hashmap  14593  hashfun  14595  hashbclem  14610  hashfacen  14612  hashf1lem2  14614  hashf1  14615  ccatsymb  14741  swrdwrdsymb  14826  swrdsb0eq  14827  ccatpfx  14864  swrdswrd  14868  wrdind  14885  wrd2ind  14886  swrdccatin1  14888  swrdccatin2  14892  pfxccatin12lem2  14894  pfxccatin12  14896  swrdccat  14898  repswswrd  14949  0csh0  14958  cshwidxmod  14968  2cshw  14978  cshweqrep  14986  relexp0g  15190  relexpsucnnr  15193  relexpindlem  15231  01sqrexlem1  15424  01sqrexlem6  15429  rlim  15677  rlimclim1  15727  climsup  15852  caurcvg2  15860  caucvgb  15862  iseralt  15867  sumss  15905  fsum2dlem  15951  mptfzshft  15959  modfsummod  15976  o1fsum  15995  incexclem  16020  divrcnv  16036  flo1  16038  fprodrev  16159  fprod2dlem  16162  ruclem6  16418  moddvds  16448  dvdsaddre2b  16492  dvdsflip  16502  addmodlteqALT  16510  nn0o  16568  fldivndvdslt  16601  bitsf1ocnv  16629  bitsf1  16631  sadcaddlem  16642  bezoutlem2  16728  bezoutlem4  16730  lcmgcdlem  16796  prmind2  16875  isprm5  16898  isprm6  16905  prmdvdsncoprmbd  16918  cncongrprm  16920  hashdvds  16967  crth  16970  eulerthlem2  16974  prmdiveq  16978  hashgcdlem  16980  hashgcdeq  16982  iserodd  17028  pclem  17031  pcprendvds2  17034  pcexp  17052  pcneg  17067  pc2dvds  17072  pcmpt  17085  prmpwdvds  17097  pockthg  17099  prmreclem5  17113  4sqlem11  17148  ramub2  17207  ramubcl  17211  ram0  17215  ramub1lem2  17220  ramcl  17222  prmgaplem3  17246  prmgaplem6  17249  setscom  17373  sscpwex  18005  initoeu2  18206  setcinv  18280  funcestrcsetclem9  18337  funcsetcestrclem9  18352  fullsetcestrc  18355  1stfcl  18386  2ndfcl  18387  hofpropd  18456  isacs3lem  18731  isacs4lem  18733  acsmap2d  18744  chnflenfi  18817  subsubmgm  18914  submnd0OLD  18972  mndpsuppss  18974  subsubm  19027  insubm  19029  frmdup1  19075  frmdup3lem  19077  sgrp2nmndlem2  19138  isgrpinv  19219  subsubg  19375  cycsubgcl  19436  conjghm  19478  qusghm  19484  gsumwrev  19595  gsmsymgrfixlem1  19656  symgfixelsi  19664  symgsssg  19696  symgfisg  19697  psgnunilem2  19724  odf1o2  19802  sylow1lem1  19827  odcau  19833  pgpfi  19834  pgpssslw  19843  fislw  19854  efgtlen  19955  efginvrel2  19956  efgrelexlemb  19979  efgredeu  19981  efgcpbllemb  19984  frgpup1  20004  lt6abl  20124  gsum2d  20201  gsum2d2lem  20202  gsum2d2  20203  telgsumfzslem  20217  dmdprdsplit2lem  20276  ablfacrp  20297  pgpfac1lem3  20308  gsummgp0  20562  irredrmul  20672  subsubrng  20830  subsubrg  20865  rngcinv  20904  ringcinv  20938  fldhmsubc  21057  islss4  21252  lspextmo  21346  lspsnat  21438  prmirredlem  21793  znf1o  21872  znidomb  21882  frgpcyg  21894  psgnghm  21901  psgndiflemB  21921  frlmlbs  22118  frlmup1  22119  lindfind  22137  islindf3  22147  lindfmm  22148  issubassa3  22189  resspsradd  22297  resspsrmul  22298  psdmul  22502  coe1tmmul2  22610  pf1ind  22688  mamulid  22771  mat1dimelbas  22801  mdetdiaglem  22928  mdetralt2  22939  mndifsplit  22966  smadiadetglem2  23002  matunitlindflem2  23010  1elcpmat  23048  pmatcollpw3lem  23116  chfacfisf  23187  chfacfisfcpmat  23188  chfacffsupp  23189  chfacfscmulfsupp  23192  chfacfscmulgsum  23193  chfacfpmmulfsupp  23196  chfacfpmmulgsum  23197  chfacfpmmulgsum2  23198  cayhamlem1  23199  cpmadugsumlemF  23209  cayleyhamilton1  23225  tgcl  23302  pptbas  23341  clsval2  23383  mretopd  23425  lmbr2  23592  cncls2  23606  nrmsep  23690  regsep2  23709  cmpsublem  23732  cmpsub  23733  tgcmp  23734  uncmp  23736  hauscmplem  23739  iunconnlem  23760  1stcrest  23786  2ndcctbss  23789  2ndcsep  23793  dis2ndc  23794  hausllycmp  23828  dislly  23831  kgentopon  23872  1stckgen  23888  kgencn3  23892  ptpjpre1  23905  ptbasin  23911  ptpjopn  23946  dfac14  23952  ptcnplem  23955  txcn  23960  txindis  23968  txdis1cn  23969  ptrescn  23973  txcmplem1  23975  txcmp  23977  txhaus  23981  txlm  23982  tx1stc  23984  txkgen  23986  xkococn  23994  qtopcn  24048  kqreglem1  24075  kqreglem2  24076  kqnrmlem1  24077  kqnrmlem2  24078  hmeoimaf1o  24104  reghmph  24127  nrmhmph  24128  txhmeo  24137  ptuncnv  24141  filconn  24217  fbasrn  24218  fmfnfmlem2  24289  flimfnfcls  24362  cnpfcfi  24374  alexsublem  24378  alexsubALTlem2  24382  alexsubALTlem3  24383  alexsubALTlem4  24384  alexsubALT  24385  ptcmplem3  24388  cnextfval  24396  tsmsxp  24489  imasdsf1olem  24707  bl2in  24734  blssps  24758  blss  24759  blssexps  24760  blssex  24761  blcld  24839  stdbdxmet  24849  met1stc  24855  prdsxmslem2  24863  metcnp3  24874  metcnpi3  24880  txmetcnp  24881  nmo0  25069  nmoid  25076  icccmplem1  25157  icccmp  25160  xrge0tsms  25169  metdseq0  25189  cnheiborlem  25290  cnheibor  25291  cnllycmp  25292  pcoval2  25352  cmetcaulem  25624  iscmet3lem1  25627  iscmet3lem2  25628  equivcau  25636  lmcau  25649  cncmet  25658  ivthlem2  25788  ivthlem3  25789  ovoliunlem2  25839  ovolscalem2  25850  uniioombl  25925  dyaddisj  25932  opnmbllem  25937  volivth  25943  ismbfd  25975  ismbf3d  25990  mbfimaopnlem  25991  mbfinf  26001  itg1addlem4  26035  mbfi1fseqlem1  26051  mbfi1fseqlem3  26053  mbfi1fseqlem4  26054  mbfi1fseqlem5  26055  mbfi1fseqlem6  26056  itg2seq  26078  itg2lea  26080  itg2split  26085  itg2cnlem1  26097  bddiblnc  26177  limciun  26229  dvmptfsum  26310  rolle  26325  c1lip1  26332  dvcnvrelem1  26352  dvcnvre  26354  dvcvx  26355  itgsubst  26384  tdeglem4  26393  mdegmullem  26411  plyco0  26525  coemullem  26584  dgreq0  26599  dgrmul  26604  dgrco  26609  elqaalem2  26658  preimaaa  26661  aannenlem1  26670  aaliou3lem9  26692  ulmres  26730  ulmshftlem  26731  angneg  27146  dcubic  27189  cxploglim  27320  cxploglim2  27321  scvxcvx  27328  lgamgulmlem5  27375  lgamcvg2  27397  ftalem2  27416  basellem3  27425  basellem4  27426  sqff1o  27524  fsumdvdsdiaglem  27525  dvdsflsumcom  27530  mpodvdsmulf1o  27536  dvdsmulf1o  27538  fsumvma2  27556  logfac2  27559  logfacrlim  27566  logexprlim  27567  dchrelbasd  27581  lgsne0  27677  lgsqrlem2  27689  lgsqrmodndvds  27695  gausslemma2dlem1a  27707  lgseisenlem2  27718  lgsquadlem1  27722  lgsquadlem2  27723  lgsquadlem3  27724  lgsquad2lem2  27727  2sqlem8  27768  2sqlem11  27771  2sqreultlem  27789  2sqreunnltlem  27792  chpo1ubb  27823  vmadivsum  27824  rplogsumlem2  27827  rpvmasumlem  27829  dchrmusum2  27836  dchrvmasumlem1  27837  dchrisum0fno1  27853  dchrisum0re  27855  dchrisum0lem1  27858  dchrisum0lem2  27860  dchrisum0lem3  27861  dchrisum0  27862  mulogsumlem  27873  mulog2sumlem2  27877  vmalogdivsum2  27880  logsqvma  27884  log2sumbnd  27886  selberglem3  27889  selberg  27890  selberg2lem  27892  selberg2b  27894  selberg3lem2  27900  pntrmax  27906  pntrsumo1  27907  pntlemn  27942  pntlemp  27952  qabvle  27967  ostthlem1  27969  ostthlem2  27970  ostth2lem2  27976  ostth3  27980  ltsres  28034  nosupno  28075  nosupbnd2  28088  noinfno  28090  noinfbnd2  28103  etaslts  28194  cuteq1  28218  addsproplem2  28371  mulsval  28510  precsexlem11  28618  n0fincut  28756  zmulscld  28798  bdayfinbndlem1  28868  idmot  29015  plngval  29270  brbtwn2  29498  colinearalglem4  29502  colinearalg  29503  ax5seglem9  29530  axpaschlem  29533  axcontlem2  29558  axcontlem7  29563  axcontlem8  29564  eengtrkg  29579  upgr1eopALT  29710  uspgredg2vlem  29819  subumgr  29884  nbgr0edglem  29952  edgnbusgreu  29963  nb3grprlem1  29976  wlkl1loop  30233  pthdivtx  30327  usgr2pth  30365  crctcshwlkn0  30425  wlklnwwlkln1  30472  wwlksnext  30497  clwwlkccatlem  30595  clwlkclwwlklem2a  30604  clwwlkinwwlk  30646  clwwlkn1loopb  30649  clwwlkf  30653  wwlksext2clwwlk  30663  wwlksubclwwlk  30664  clwwlknscsh  30668  clwwlknon1  30703  clwwlknonex2e  30716  1conngr  30810  n4cyclfrgr  30907  numclwwlk2lem1lem  30958  2clwwlk2clwwlk  30966  numclwwlk1lem2f1  30973  numclwlk1lem1  30985  numclwwlk2lem1  30992  numclwlk2lem2f  30993  numclwwlk7  31007  frgrogt3nreg  31013  grpoidinvlem1  31121  grpoidinvlem3  31123  grporcan  31135  nmlnoubi  31413  blocnilem  31421  ipblnfi  31472  htthlem  31534  ocsh  31900  shmodsi  32006  pjhthlem2  32009  5oalem2  32272  eigposi  32453  nmopub2tALT  32526  nmfnleub2  32543  nmcexi  32643  nmopcoi  32712  kbass3  32735  mdslmd1lem1  32942  mdslmd1lem2  32943  chirredlem2  33008  chirredlem4  33010  mdsymlem3  33022  mdsymlem5  33024  sumdmdii  33032  sumdmdlem  33035  sumdmdlem2  33036  foresf1o  33157  disjxpin  33239  1stpreimas  33356  resf1o  33378  nn0xmulclb  33419  wrdt2ind  33572  xrge0tsmsd  33690  gsumvsca1  33843  gsumvsca2  33844  islinds5  33979  1arithidomlem2  34124  mplvrpmmhm  34234  irngnzply1  34379  mdetpmtr1  34511  mdetpmtr2  34512  pstmxmet  34585  qqhghm  34676  qqhrhm  34677  esumpcvgval  34766  volmeas  34920  imambfm  34950  dya2iocnrect  34969  oddpwdc  35042  sseqf  35080  orvcgteel  35156  orvclteel  35161  ballotlemsf1o  35202  bnj1110  35668  bnj1118  35670  txpconn  36121  connpconn  36124  cnllysconn  36134  rellysconn  36140  cvmsss2  36163  cvmlift2lem9  36200  satf00  36263  fmlasuc  36275  mrsubfval  36397  mppsval  36461  dfon2lem6  36680  wzel  36716  ifscgr  36939  cgrxfr  36950  btwnconn1lem5  36986  btwnconn1lem6  36987  btwnconn1lem12  36993  brsegle  37003  finminlem  37236  nn0prpwlem  37240  fnessref  37275  refssfne  37276  neibastop1  37277  topjoin  37283  fnemeet2  37285  weiunse  37386  bj-prmoore  38178  bj-finsumval0  38349  topdifinffinlem  38413  lindsadd  38679  poimirlem28  38709  poimirlem32  38713  opnmbllem0  38717  mblfinlem1  38718  mblfinlem4  38721  ismblfin  38722  mbfresfi  38727  itg2addnclem  38732  itg2addnclem3  38734  itg2addnc  38735  unirep  38791  frinfm  38812  sdclem2  38819  geomcau  38836  istotbnd3  38848  sstotbnd2  38851  sstotbnd  38852  sstotbnd3  38853  totbndbnd  38866  cntotbnd  38873  ismtyres  38885  heibor1lem  38886  heiborlem1  38888  heiborlem8  38895  ismndo1  38950  isdivrngo  39027  unichnidl  39108  erimeq2  39838  cvlcvr1  40539  ishlat3N  40554  llnmlplnN  40739  islvol2aN  40792  4atlem4c  40801  4atlem4d  40802  isline2  40974  isline3  40976  linepsubclN  41151  lhpexle3lem  41211  lhpjat2  41221  cdlemd4  41401  cdleme0cq  41415  cdleme32fva  41637  cdleme32fvaw  41639  tendo0mul  42026  tendo0mulr  42027  diameetN  42256  dvhvaddcl  42295  dvhvaddcomN  42296  cdlemm10N  42318  dvadiaN  42328  djavalN  42335  dihvalcqat  42439  dihopelvalcpre  42448  djhval  42598  dihjat1lem  42628  sticksstones11  43349  sticksstones22  43361  remul01  43601  zaddcom  43671  zmulcom  43675  fidomncyc  43742  evlselvlem  43759  evlselv  43760  fsuppind  43761  mhpind  43765  prjspertr  43776  prjsprellsp  43782  elrfi  43848  nacsfix  43866  fzsplit1nn0  43908  eldioph2  43916  lzenom  43924  irrapxlem3  43974  pellexlem5  43983  pell1234qrne0  44003  pell1234qrmulcl  44005  pell14qrdich  44019  pell1qrge1  44020  pellqrex  44029  reglogltb  44041  reglogleb  44042  rmxypairf1o  44061  rmxycomplete  44067  monotoddzzfi  44092  congadd  44116  congsym  44118  acongrep  44130  jm2.19lem3  44141  jm2.19lem4  44142  jm2.22  44145  jm2.25  44149  expdiophlem1  44171  wepwsolem  44192  kelac1  44208  lmhmfgsplit  44231  pwslnm  44239  hbtlem6  44274  hbt  44275  mon1psubm  44344  deg1mhm  44345  omord2lim  44445  succlg  44473  onmcl  44476  ofoafo  44501  ofoacom  44506  fzunt  44599  fzuntd  44600  fzunt1d  44601  fzuntgd  44602  iunrelexp0  44845  dssmapnvod  45163  gsumws3  45339  gsumws4  45340  mulltgt0  46181  fnchoice  46188  disjrnmpt2  46345  fzisoeu  46458  fsumiunss  46729  climinf  46760  mullimc  46770  mullimcf  46777  stoweidlem14  47166  stoweidlem17  47169  stoweidlem34  47186  stoweidlem50  47202  fourierdlem42  47301  fourierdlem62  47320  fourierdlem71  47329  fourierdlem76  47334  qndenserrnbllem  47446  subsaliuncl  47510  sge0resplit  47558  3f1oss1  48287  2reu8i  48326  addmodne  48562  fundcmpsurinjpreimafv  48632  iccpartigtl  48647  prproropf1olem2  48728  prproropf1olem4  48730  paireqne  48735  prmdvdsfmtnof1lem2  48812  nprmdvdsfacm1  48851  bgoldbtbndlem3  49047  bgoldbtbnd  49049  grimcnv  49128  gricushgr  49157  cycldlenngric  49168  grimedg  49175  grtrimap  49188  isubgr3stgrlem6  49211  isubgr3stgrlem7  49212  isubgr3stgrlem8  49213  isubgr3stgrlem9  49214  grlimfn  49219  gpgedg2iv  49307  gpg5nbgrvtx03starlem2  49309  gpg5nbgrvtx13starlem2  49312  uspgrsprf1  49387  isassintop  49449  2zlidl  49479  2zrngnmrid  49495  rngcinvALTV  49515  funcringcsetcALTV2lem9  49537  ringcinvALTV  49549  funcringcsetclem9ALTV  49560  fldhmsubcALTV  49572  gsumlsscl  49634  lincsum  49683  lindslinindsimp1  49711  lindslinindimp2lem4  49715  lincresunitlem2  49730  elfzolborelfzop1  49773  elbigo2  49806  digexp  49861  dig1  49862  nn0sumshdiglemB  49874  1arymaptf1  49896  2arymaptf1  49907  itcoval1  49917  itcoval2  49918  itcoval3  49919  itcovalsucov  49922  ackvalsuc1mpt  49932  itschlc0xyqsol  50021  itscnhlinecirc02p  50039  brab2dd  50081  dmrnxp  50090  xpco2  50110  initopropd  50507  termopropd  50508  zeroopropd  50509  prcofpropd  50656  thincciso  50730  indthinc  50739  indthincALT  50740  oduoppcciso  50846  lanpropd  50940  ranpropd  50941