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  5099  reusv2lem4  5351  axprlem5OLD  5380  fr2nr  5608  somin1  6094  tz7.7  6346  f1oprg  6827  soisores  7284  elovmporab1w  7616  elovmporab1  7617  sorpssi  7685  onint  7746  ordsucelsuc  7777  elxp5  7879  resf1extb  7890  f1oabexg  7898  wemoiso  7931  wemoiso2  7932  el2xptp0  7994  frxp2  8100  frxp3  8107  ressuppss  8139  fprlem1  8256  tz7.48lem  8386  oalimcl  8501  oeeui  8543  nnaordex2  8580  oaabs2  8590  omabs  8592  swoer  8679  ralxpmap  8846  pw2f1olem  9022  enfixsn  9027  mapxpen  9084  mapunen  9087  php  9148  unxpdomlem2  9174  unxpdomlem3  9175  findcard3OLD  9206  isfinite2  9221  fodomfi  9237  domunfican  9248  fodomfiOLD  9257  fissuni  9284  fipreima  9285  indexfi  9287  fsuppsssupp  9308  marypha1lem  9360  marypha2  9366  supmo  9379  infmo  9424  oieu  9468  brwdom2  9502  ixpiunwdom  9519  cantnfval2  9598  cantnfle  9600  cantnflt  9601  cantnf  9622  wemapwe  9626  cnfcom  9629  frrlem15  9686  rankonidlem  9757  r1pwcl  9776  eldju2ndl  9853  eldju2ndr  9854  djuun  9855  infxpenlem  9942  infxpenc2lem1  9948  fseqenlem1  9953  dfac8clem  9961  mappwen  10041  dfac3  10050  dfac5  10058  dfac12lem3  10075  infunsdom  10142  coftr  10202  ssfin4  10239  domfin4  10240  fin23lem26  10254  fin23lem22  10256  fin23lem28  10269  fin23lem32  10273  fin23lem40  10280  isf32lem5  10286  compssiso  10303  isf34lem4  10306  isfin1-3  10315  fin1a2lem13  10341  hsmexlem2  10356  hsmexlem4  10358  zorn2lem1  10425  ttukeylem6  10443  iundom2g  10469  konigthlem  10497  pwcfsdom  10512  fpwwe2lem11  10570  fpwwe2  10572  pwfseqlem3  10589  winalim2  10625  r1wunlim  10666  inttsk  10703  inar1  10704  grur1  10749  nqereq  10864  ltexprlem7  10971  prlem936  10976  00id  11325  addlid  11333  ltord1  11680  divdiv1  11869  divdiv2  11870  conjmul  11875  ltdivmul  12034  ledivmul  12035  lt2mul2div  12037  ltdiv23  12050  lediv23  12051  lediv12a  12052  ledivp1  12061  negfi  12108  nn0nndivcl  12490  nn0ge0div  12579  peano2uz2  12598  peano5uzi  12599  eluzp1m1  12795  qbtwnre  13135  xralrple  13141  xleadd1a  13189  xmulge0  13220  xmulass  13223  xlemul1a  13224  iooshf  13363  divelunit  13431  eluzgtdifelfzo  13664  modadd1  13846  modmul1  13865  seqcl2  13961  seqfveq2  13965  seqid2  13989  seqhomo  13990  seqdistr  13994  mulexpz  14043  leexp2r  14115  expnlbnd2  14175  expmulnbnd  14176  hashmap  14376  hashfun  14378  hashbclem  14393  hashfacen  14395  hashf1lem2  14397  hashf1  14398  ccatsymb  14523  swrdwrdsymb  14603  swrdsb0eq  14604  ccatpfx  14642  swrdswrd  14646  wrdind  14663  wrd2ind  14664  swrdccatin1  14666  swrdccatin2  14670  pfxccatin12lem2  14672  pfxccatin12  14674  swrdccat  14676  repswswrd  14725  0csh0  14734  cshwidxmod  14744  2cshw  14754  cshweqrep  14762  relexp0g  14964  relexpsucnnr  14967  relexpindlem  15005  01sqrexlem1  15184  01sqrexlem6  15189  rlim  15437  rlimclim1  15487  climsup  15612  caurcvg2  15620  caucvgb  15622  iseralt  15627  sumss  15666  fsum2dlem  15712  mptfzshft  15720  modfsummod  15736  o1fsum  15755  incexclem  15778  divrcnv  15794  flo1  15796  fprodrev  15919  fprod2dlem  15922  ruclem6  16179  moddvds  16209  dvdsaddre2b  16253  dvdsflip  16263  addmodlteqALT  16271  nn0o  16329  fldivndvdslt  16362  bitsf1ocnv  16390  bitsf1  16392  sadcaddlem  16403  bezoutlem2  16486  bezoutlem4  16488  lcmgcdlem  16552  prmind2  16631  isprm5  16653  isprm6  16660  prmdvdsncoprmbd  16673  cncongrprm  16675  hashdvds  16721  crth  16724  eulerthlem2  16728  prmdiveq  16732  hashgcdlem  16734  hashgcdeq  16736  iserodd  16782  pclem  16785  pcprendvds2  16788  pcexp  16806  pcneg  16821  pc2dvds  16826  pcmpt  16839  prmpwdvds  16851  pockthg  16853  prmreclem5  16867  4sqlem11  16902  ramub2  16961  ramubcl  16965  ram0  16969  ramub1lem2  16974  ramcl  16976  prmgaplem3  17000  prmgaplem6  17003  setscom  17126  sscpwex  17757  initoeu2  17958  setcinv  18032  funcestrcsetclem9  18089  funcsetcestrclem9  18104  fullsetcestrc  18107  1stfcl  18138  2ndfcl  18139  hofpropd  18208  isacs3lem  18483  isacs4lem  18485  acsmap2d  18496  subsubmgm  18619  submnd0  18672  mndpsuppss  18674  subsubm  18725  insubm  18727  frmdup1  18773  frmdup3lem  18775  sgrp2nmndlem2  18833  isgrpinv  18907  subsubg  19063  cycsubgcl  19120  conjghm  19163  qusghm  19169  gsumwrev  19280  gsmsymgrfixlem1  19341  symgfixelsi  19349  symgsssg  19381  symgfisg  19382  psgnunilem2  19409  odf1o2  19487  sylow1lem1  19512  odcau  19518  pgpfi  19519  pgpssslw  19528  fislw  19539  efgtlen  19640  efginvrel2  19641  efgrelexlemb  19664  efgredeu  19666  efgcpbllemb  19669  frgpup1  19689  lt6abl  19809  gsum2d  19886  gsum2d2lem  19887  gsum2d2  19888  telgsumfzslem  19902  dmdprdsplit2lem  19961  ablfacrp  19982  pgpfac1lem3  19993  gsummgp0  20238  irredrmul  20347  subsubrng  20483  subsubrg  20518  rngcinv  20557  ringcinv  20591  fldhmsubc  20705  islss4  20900  lspextmo  20995  lspsnat  21087  prmirredlem  21414  znf1o  21493  znidomb  21503  frgpcyg  21515  psgnghm  21522  psgndiflemB  21542  frlmlbs  21739  frlmup1  21740  lindfind  21758  islindf3  21768  lindfmm  21769  issubassa3  21808  resspsradd  21917  resspsrmul  21918  psdmul  22086  coe1tmmul2  22195  pf1ind  22275  mamulid  22361  mat1dimelbas  22391  mdetdiaglem  22518  mdetralt2  22529  mndifsplit  22556  smadiadetglem2  22592  1elcpmat  22635  pmatcollpw3lem  22703  chfacfisf  22774  chfacfisfcpmat  22775  chfacffsupp  22776  chfacfscmulfsupp  22779  chfacfscmulgsum  22780  chfacfpmmulfsupp  22783  chfacfpmmulgsum  22784  chfacfpmmulgsum2  22785  cayhamlem1  22786  cpmadugsumlemF  22796  cayleyhamilton1  22812  tgcl  22889  pptbas  22928  clsval2  22970  mretopd  23012  lmbr2  23179  cncls2  23193  nrmsep  23277  regsep2  23296  cmpsublem  23319  cmpsub  23320  tgcmp  23321  uncmp  23323  hauscmplem  23326  iunconnlem  23347  1stcrest  23373  2ndcctbss  23375  2ndcsep  23379  dis2ndc  23380  hausllycmp  23414  dislly  23417  kgentopon  23458  1stckgen  23474  kgencn3  23478  ptpjpre1  23491  ptbasin  23497  ptpjopn  23532  dfac14  23538  ptcnplem  23541  txcn  23546  txindis  23554  txdis1cn  23555  ptrescn  23559  txcmplem1  23561  txcmp  23563  txhaus  23567  txlm  23568  tx1stc  23570  txkgen  23572  xkococn  23580  qtopcn  23634  kqreglem1  23661  kqreglem2  23662  kqnrmlem1  23663  kqnrmlem2  23664  hmeoimaf1o  23690  reghmph  23713  nrmhmph  23714  txhmeo  23723  ptuncnv  23727  filconn  23803  fbasrn  23804  fmfnfmlem2  23875  flimfnfcls  23948  cnpfcfi  23960  alexsublem  23964  alexsubALTlem2  23968  alexsubALTlem3  23969  alexsubALTlem4  23970  alexsubALT  23971  ptcmplem3  23974  cnextfval  23982  tsmsxp  24075  imasdsf1olem  24294  bl2in  24321  blssps  24345  blss  24346  blssexps  24347  blssex  24348  blcld  24426  stdbdxmet  24436  met1stc  24442  prdsxmslem2  24450  metcnp3  24461  metcnpi3  24467  txmetcnp  24468  nmo0  24656  nmoid  24663  icccmplem1  24744  icccmp  24747  xrge0tsms  24756  metdseq0  24776  cnheiborlem  24886  cnheibor  24887  cnllycmp  24888  pcoval2  24949  cmetcaulem  25221  iscmet3lem1  25224  iscmet3lem2  25225  equivcau  25233  lmcau  25246  cncmet  25255  ivthlem2  25386  ivthlem3  25387  ovoliunlem2  25437  ovolscalem2  25448  uniioombl  25523  dyaddisj  25530  opnmbllem  25535  volivth  25541  ismbfd  25573  ismbf3d  25588  mbfimaopnlem  25589  mbfinf  25599  itg1addlem4  25633  mbfi1fseqlem1  25649  mbfi1fseqlem3  25651  mbfi1fseqlem4  25652  mbfi1fseqlem5  25653  mbfi1fseqlem6  25654  itg2seq  25676  itg2lea  25678  itg2split  25683  itg2cnlem1  25695  bddiblnc  25776  limciun  25828  dvmptfsum  25912  rolle  25927  c1lip1  25935  dvcnvrelem1  25955  dvcnvre  25957  dvcvx  25958  itgsubst  25989  tdeglem4  25998  mdegmullem  26016  plyco0  26130  coemullem  26188  dgreq0  26204  dgrmul  26209  dgrco  26214  elqaalem2  26261  aannenlem1  26269  aaliou3lem9  26291  ulmres  26330  ulmshftlem  26331  angneg  26746  dcubic  26789  cxploglim  26921  cxploglim2  26922  scvxcvx  26929  lgamgulmlem5  26976  lgamcvg2  26998  ftalem2  27017  basellem3  27026  basellem4  27027  sqff1o  27125  fsumdvdsdiaglem  27126  dvdsflsumcom  27131  mpodvdsmulf1o  27137  dvdsmulf1o  27139  fsumvma2  27158  logfac2  27161  logfacrlim  27168  logexprlim  27169  dchrelbasd  27183  lgsne0  27279  lgsqrlem2  27291  lgsqrmodndvds  27297  gausslemma2dlem1a  27309  lgseisenlem2  27320  lgsquadlem1  27324  lgsquadlem2  27325  lgsquadlem3  27326  lgsquad2lem2  27329  2sqlem8  27370  2sqlem11  27373  2sqreultlem  27391  2sqreunnltlem  27394  chpo1ubb  27425  vmadivsum  27426  rplogsumlem2  27429  rpvmasumlem  27431  dchrmusum2  27438  dchrvmasumlem1  27439  dchrisum0fno1  27455  dchrisum0re  27457  dchrisum0lem1  27460  dchrisum0lem2  27462  dchrisum0lem3  27463  dchrisum0  27464  mulogsumlem  27475  mulog2sumlem2  27479  vmalogdivsum2  27482  logsqvma  27486  log2sumbnd  27488  selberglem3  27491  selberg  27492  selberg2lem  27494  selberg2b  27496  selberg3lem2  27502  pntrmax  27508  pntrsumo1  27509  pntlemn  27544  pntlemp  27554  qabvle  27569  ostthlem1  27571  ostthlem2  27572  ostth2lem2  27578  ostth3  27582  sltres  27607  nosupno  27648  nosupbnd2  27661  noinfno  27663  noinfbnd2  27676  etasslt  27759  cuteq1  27783  addsproplem2  27917  mulsval  28052  precsexlem11  28159  n0sfincut  28286  zmulscld  28325  idmot  28517  brbtwn2  28885  colinearalglem4  28889  colinearalg  28890  ax5seglem9  28917  axpaschlem  28920  axcontlem2  28945  axcontlem7  28950  axcontlem8  28951  eengtrkg  28966  upgr1eopALT  29097  uspgredg2vlem  29203  subumgr  29268  nbgr0edglem  29336  edgnbusgreu  29347  nb3grprlem1  29360  wlkl1loop  29618  pthdivtx  29707  usgr2pth  29744  crctcshwlkn0  29801  wlklnwwlkln1  29848  wwlksnext  29873  clwwlkccatlem  29968  clwlkclwwlklem2a  29977  clwwlkinwwlk  30019  clwwlkn1loopb  30022  clwwlkf  30026  wwlksext2clwwlk  30036  wwlksubclwwlk  30037  clwwlknscsh  30041  clwwlknon1  30076  clwwlknonex2e  30089  1conngr  30173  n4cyclfrgr  30270  numclwwlk2lem1lem  30321  2clwwlk2clwwlk  30329  numclwwlk1lem2f1  30336  numclwlk1lem1  30348  numclwwlk2lem1  30355  numclwlk2lem2f  30356  numclwwlk7  30370  frgrogt3nreg  30376  grpoidinvlem1  30483  grpoidinvlem3  30485  grporcan  30497  nmlnoubi  30775  blocnilem  30783  ipblnfi  30834  htthlem  30896  ocsh  31262  shmodsi  31368  pjhthlem2  31371  5oalem2  31634  eigposi  31815  nmopub2tALT  31888  nmfnleub2  31905  nmcexi  32005  nmopcoi  32074  kbass3  32097  mdslmd1lem1  32304  mdslmd1lem2  32305  chirredlem2  32370  chirredlem4  32372  mdsymlem3  32384  mdsymlem5  32386  sumdmdii  32394  sumdmdlem  32397  sumdmdlem2  32398  foresf1o  32483  disjxpin  32567  1stpreimas  32679  resf1o  32703  nn0xmulclb  32744  wrdt2ind  32925  xrge0tsmsd  33045  gsumvsca1  33195  gsumvsca2  33196  islinds5  33331  1arithidomlem2  33500  irngnzply1  33679  mdetpmtr1  33806  mdetpmtr2  33807  pstmxmet  33880  qqhghm  33971  qqhrhm  33972  esumpcvgval  34061  volmeas  34214  imambfm  34246  dya2iocnrect  34265  oddpwdc  34338  sseqf  34376  orvcgteel  34452  orvclteel  34457  ballotlemsf1o  34498  bnj1110  34965  bnj1118  34967  f1resveqaeq  35068  txpconn  35212  connpconn  35215  cnllysconn  35225  rellysconn  35231  cvmsss2  35254  cvmlift2lem9  35291  satf00  35354  fmlasuc  35366  mrsubfval  35488  mppsval  35552  dfon2lem6  35769  wzel  35805  ifscgr  36025  cgrxfr  36036  btwnconn1lem5  36072  btwnconn1lem6  36073  btwnconn1lem12  36079  brsegle  36089  finminlem  36299  nn0prpwlem  36303  fnessref  36338  refssfne  36339  neibastop1  36340  topjoin  36346  fnemeet2  36348  weiunse  36449  bj-prmoore  37096  bj-finsumval0  37266  topdifinffinlem  37328  lindsadd  37600  matunitlindflem2  37604  poimirlem28  37635  poimirlem32  37639  opnmbllem0  37643  mblfinlem1  37644  mblfinlem4  37647  ismblfin  37648  mbfresfi  37653  itg2addnclem  37658  itg2addnclem3  37660  itg2addnc  37661  unirep  37701  frinfm  37722  sdclem2  37729  geomcau  37746  istotbnd3  37758  sstotbnd2  37761  sstotbnd  37762  sstotbnd3  37763  totbndbnd  37776  cntotbnd  37783  ismtyres  37795  heibor1lem  37796  heiborlem1  37798  heiborlem8  37805  ismndo1  37860  isdivrngo  37937  unichnidl  38018  erimeq2  38663  cvlcvr1  39325  ishlat3N  39340  llnmlplnN  39526  islvol2aN  39579  4atlem4c  39588  4atlem4d  39589  isline2  39761  isline3  39763  linepsubclN  39938  lhpexle3lem  39998  lhpjat2  40008  cdlemd4  40188  cdleme0cq  40202  cdleme32fva  40424  cdleme32fvaw  40426  tendo0mul  40813  tendo0mulr  40814  diameetN  41043  dvhvaddcl  41082  dvhvaddcomN  41083  cdlemm10N  41105  dvadiaN  41115  djavalN  41122  dihvalcqat  41226  dihopelvalcpre  41235  djhval  41385  dihjat1lem  41415  sticksstones11  42137  sticksstones22  42149  f1o2d2  42214  remul01  42388  zaddcom  42445  zmulcom  42449  fidomncyc  42516  evlselvlem  42567  evlselv  42568  fsuppind  42571  mhpind  42575  prjspertr  42586  prjsprellsp  42592  elrfi  42675  nacsfix  42693  fzsplit1nn0  42735  eldioph2  42743  lzenom  42751  irrapxlem3  42805  pellexlem5  42814  pell1234qrne0  42834  pell1234qrmulcl  42836  pell14qrdich  42850  pell1qrge1  42851  pellqrex  42860  reglogltb  42872  reglogleb  42873  rmxypairf1o  42893  rmxycomplete  42899  monotoddzzfi  42924  congadd  42948  congsym  42950  acongrep  42962  jm2.19lem3  42973  jm2.19lem4  42974  jm2.22  42977  jm2.25  42981  expdiophlem1  43003  wepwsolem  43024  kelac1  43045  lmhmfgsplit  43068  pwslnm  43076  hbtlem6  43111  hbt  43112  mon1psubm  43181  deg1mhm  43182  omord2lim  43282  succlg  43310  onmcl  43313  ofoafo  43338  ofoacom  43343  fzunt  43437  fzuntd  43438  fzunt1d  43439  fzuntgd  43440  iunrelexp0  43684  dssmapnvod  44002  gsumws3  44178  gsumws4  44179  mulltgt0  45009  fnchoice  45016  disjrnmpt2  45175  fzisoeu  45291  fsumiunss  45566  climinf  45597  mullimc  45607  mullimcf  45614  stoweidlem14  46005  stoweidlem17  46008  stoweidlem34  46025  stoweidlem50  46041  fourierdlem42  46140  fourierdlem62  46159  fourierdlem71  46168  fourierdlem76  46173  qndenserrnbllem  46285  subsaliuncl  46349  sge0resplit  46397  upwrdfi  46878  3f1oss1  47069  2reu8i  47107  addmodne  47338  fundcmpsurinjpreimafv  47402  iccpartigtl  47417  prproropf1olem2  47498  prproropf1olem4  47500  paireqne  47505  prmdvdsfmtnof1lem2  47579  bgoldbtbndlem3  47801  bgoldbtbnd  47803  grimcnv  47881  gricushgr  47910  cycldlenngric  47921  grimedg  47928  grtrimap  47940  isubgr3stgrlem6  47963  isubgr3stgrlem7  47964  isubgr3stgrlem8  47965  isubgr3stgrlem9  47966  grlimfn  47971  gpgedg2iv  48051  gpg5nbgrvtx03starlem2  48053  gpg5nbgrvtx13starlem2  48056  uspgrsprf1  48128  isassintop  48191  2zlidl  48221  2zrngnmrid  48237  rngcinvALTV  48257  funcringcsetcALTV2lem9  48279  ringcinvALTV  48291  funcringcsetclem9ALTV  48302  fldhmsubcALTV  48314  gsumlsscl  48361  lincsum  48411  lindslinindsimp1  48439  lindslinindimp2lem4  48443  lincresunitlem2  48458  elfzolborelfzop1  48501  elbigo2  48534  digexp  48589  dig1  48590  nn0sumshdiglemB  48602  1arymaptf1  48624  2arymaptf1  48635  itcoval1  48645  itcoval2  48646  itcoval3  48647  itcovalsucov  48650  ackvalsuc1mpt  48660  itschlc0xyqsol  48749  brab2dd  48809  dmrnxp  48818  xpco2  48838  initopropd  49225  termopropd  49226  zeroopropd  49227  prcofpropd  49361  thincciso  49435  indthinc  49444  indthincALT  49445  oduoppcciso  49548  lanpropd  49597  ranpropd  49598