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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  simprl  769  simprll  777  simprlr  778  simprl1  1214  simprl2  1215  simprl3  1216  disjxiun  5063  reusv2lem4  5302  axprlem5  5328  fr2nr  5533  somin1  5993  tz7.7  6217  f1oprg  6659  soisores  7080  elovmporab1w  7392  elovmporab1  7393  sorpssi  7455  onint  7510  ordsucelsuc  7537  elxp5  7628  wemoiso  7674  wemoiso2  7675  el2xptp0  7736  ressuppss  7849  imacosuppOLD  7875  tz7.48lem  8077  oalimcl  8186  oeeui  8228  oaabs2  8272  omabs  8274  swoer  8319  ralxpmap  8460  pw2f1olem  8621  enfixsn  8626  mapxpen  8683  mapunen  8686  unxpdomlem2  8723  unxpdomlem3  8724  findcard3  8761  isfinite2  8776  domunfican  8791  fodomfi  8797  fissuni  8829  fipreima  8830  indexfi  8832  fsuppsssupp  8849  marypha1lem  8897  marypha2  8903  supmo  8916  infmo  8959  oieu  9003  brwdom2  9037  ixpiunwdom  9055  cantnfval2  9132  cantnfle  9134  cantnflt  9135  cantnf  9156  wemapwe  9160  cnfcom  9163  rankonidlem  9257  r1pwcl  9276  eldju2ndl  9353  eldju2ndr  9354  djuun  9355  infxpenlem  9439  infxpenc2lem1  9445  fseqenlem1  9450  dfac8clem  9458  mappwen  9538  dfac3  9547  dfac5  9554  dfac12lem3  9571  infunsdom  9636  coftr  9695  ssfin4  9732  domfin4  9733  fin23lem26  9747  fin23lem22  9749  fin23lem28  9762  fin23lem32  9766  fin23lem40  9773  isf32lem5  9779  compssiso  9796  isf34lem4  9799  isfin1-3  9808  fin1a2lem13  9834  hsmexlem2  9849  hsmexlem4  9851  zorn2lem1  9918  ttukeylem6  9936  iundom2g  9962  konigthlem  9990  pwcfsdom  10005  fpwwe2lem12  10063  fpwwe2  10065  pwfseqlem3  10082  winalim2  10118  r1wunlim  10159  inttsk  10196  inar1  10197  grur1  10242  nqereq  10357  ltexprlem7  10464  prlem936  10469  00id  10815  addid2  10823  ltord1  11166  divdiv1  11351  divdiv2  11352  conjmul  11357  ltdivmul  11515  ledivmul  11516  lt2mul2div  11518  ltdiv23  11531  lediv23  11532  lediv12a  11533  ledivp1  11542  negfi  11589  nn0nndivcl  11967  nn0ge0div  12052  peano2uz2  12071  peano5uzi  12072  eluzp1m1  12269  qbtwnre  12593  xralrple  12599  xleadd1a  12647  xmulge0  12678  xmulass  12681  xlemul1a  12682  iooshf  12816  divelunit  12881  eluzgtdifelfzo  13100  modadd1  13277  modmul1  13293  seqcl2  13389  seqfveq2  13393  seqid2  13417  seqhomo  13418  seqdistr  13422  mulexpz  13470  leexp2r  13539  expnlbnd2  13596  expmulnbnd  13597  hashmap  13797  hashfun  13799  hashbclem  13811  hashfacen  13813  hashf1lem2  13815  hashf1  13816  ccatsymb  13936  swrdwrdsymb  14024  swrdsb0eq  14025  ccatpfx  14063  swrdswrd  14067  wrdind  14084  wrd2ind  14085  swrdccatin1  14087  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12  14095  swrdccat  14097  repswswrd  14146  0csh0  14155  cshwidxmod  14165  2cshw  14175  cshweqrep  14183  relexp0g  14381  relexpsucnnr  14384  relexpindlem  14422  sqrlem1  14602  sqrlem6  14607  rlim  14852  rlimclim1  14902  climsup  15026  caurcvg2  15034  caucvgb  15036  iseralt  15041  sumss  15081  fsum2dlem  15125  mptfzshft  15133  modfsummod  15149  o1fsum  15168  incexclem  15191  divrcnv  15207  flo1  15209  fprodrev  15331  fprod2dlem  15334  ruclem6  15588  moddvds  15618  dvdsaddre2b  15657  dvdsflip  15667  addmodlteqALT  15675  nn0o  15734  fldivndvdslt  15765  bitsf1ocnv  15793  bitsf1  15795  sadcaddlem  15806  bezoutlem2  15888  bezoutlem4  15890  lcmgcdlem  15950  prmind2  16029  isprm5  16051  isprm6  16058  cncongrprm  16069  hashdvds  16112  crth  16115  eulerthlem2  16119  prmdiveq  16123  hashgcdlem  16125  hashgcdeq  16126  iserodd  16172  pclem  16175  pcprendvds2  16178  pcexp  16196  pcneg  16210  pc2dvds  16215  pcmpt  16228  prmpwdvds  16240  pockthg  16242  prmreclem5  16256  4sqlem11  16291  ramub2  16350  ramubcl  16354  ram0  16358  ramub1lem2  16363  ramcl  16365  prmgaplem3  16389  prmgaplem6  16392  setscom  16527  sscpwex  17085  initoeu2  17276  setcinv  17350  funcestrcsetclem9  17398  funcsetcestrclem9  17413  fullsetcestrc  17416  1stfcl  17447  2ndfcl  17448  hofpropd  17517  isacs3lem  17776  isacs4lem  17778  acsmap2d  17789  submnd0  17940  subsubm  17981  insubm  17983  frmdup1  18029  frmdup3lem  18031  sgrp2nmndlem2  18089  isgrpinv  18156  subsubg  18302  cycsubgcl  18349  conjghm  18389  qusghm  18395  gsumwrev  18494  gsmsymgrfixlem1  18555  symgfixelsi  18563  symgsssg  18595  symgfisg  18596  psgnunilem2  18623  odf1o2  18698  sylow1lem1  18723  odcau  18729  pgpfi  18730  pgpssslw  18739  fislw  18750  efgtlen  18852  efginvrel2  18853  efgrelexlemb  18876  efgredeu  18878  efgcpbllemb  18881  frgpup1  18901  cygablOLD  19011  lt6abl  19015  gsum2d  19092  gsum2d2lem  19093  gsum2d2  19094  telgsumfzslem  19108  dmdprdsplit2lem  19167  ablfacrp  19188  pgpfac1lem3  19199  gsummgp0  19358  irredrmul  19457  subsubrg  19561  islss4  19734  lspextmo  19828  lspsnat  19917  issubassa3  20097  resspsradd  20196  resspsrmul  20197  coe1tmmul2  20444  pf1ind  20518  prmirredlem  20640  znf1o  20698  znidomb  20708  frgpcyg  20720  psgnghm  20724  psgndiflemB  20744  frlmlbs  20941  frlmup1  20942  lindfind  20960  islindf3  20970  lindfmm  20971  mamulid  21050  mat1dimelbas  21080  mdetdiaglem  21207  mdetralt2  21218  mndifsplit  21245  smadiadetglem2  21281  1elcpmat  21323  pmatcollpw3lem  21391  chfacfisf  21462  chfacfisfcpmat  21463  chfacffsupp  21464  chfacfscmulfsupp  21467  chfacfscmulgsum  21468  chfacfpmmulfsupp  21471  chfacfpmmulgsum  21472  chfacfpmmulgsum2  21473  cayhamlem1  21474  cpmadugsumlemF  21484  cayleyhamilton1  21500  tgcl  21577  pptbas  21616  clsval2  21658  mretopd  21700  lmbr2  21867  cncls2  21881  nrmsep  21965  regsep2  21984  cmpsublem  22007  cmpsub  22008  tgcmp  22009  uncmp  22011  hauscmplem  22014  iunconnlem  22035  1stcrest  22061  2ndcctbss  22063  2ndcsep  22067  dis2ndc  22068  hausllycmp  22102  dislly  22105  kgentopon  22146  1stckgen  22162  kgencn3  22166  ptpjpre1  22179  ptbasin  22185  ptpjopn  22220  dfac14  22226  ptcnplem  22229  txcn  22234  txindis  22242  txdis1cn  22243  ptrescn  22247  txcmplem1  22249  txcmp  22251  txhaus  22255  txlm  22256  tx1stc  22258  txkgen  22260  xkococn  22268  qtopcn  22322  kqreglem1  22349  kqreglem2  22350  kqnrmlem1  22351  kqnrmlem2  22352  hmeoimaf1o  22378  reghmph  22401  nrmhmph  22402  txhmeo  22411  ptuncnv  22415  filconn  22491  fbasrn  22492  fmfnfmlem2  22563  flimfnfcls  22636  cnpfcfi  22648  alexsublem  22652  alexsubALTlem2  22656  alexsubALTlem3  22657  alexsubALTlem4  22658  alexsubALT  22659  ptcmplem3  22662  cnextfval  22670  tsmsxp  22763  imasdsf1olem  22983  bl2in  23010  blssps  23034  blss  23035  blssexps  23036  blssex  23037  blcld  23115  stdbdxmet  23125  met1stc  23131  prdsxmslem2  23139  metcnp3  23150  metcnpi3  23156  txmetcnp  23157  nmo0  23344  nmoid  23351  icccmplem1  23430  icccmp  23433  xrge0tsms  23442  metdseq0  23462  cnheiborlem  23558  cnheibor  23559  cnllycmp  23560  pcoval2  23620  cmetcaulem  23891  iscmet3lem1  23894  iscmet3lem2  23895  equivcau  23903  lmcau  23916  cncmet  23925  ivthlem2  24053  ivthlem3  24054  ovoliunlem2  24104  ovolscalem2  24115  uniioombl  24190  dyaddisj  24197  opnmbllem  24202  volivth  24208  ismbfd  24240  ismbf3d  24255  mbfimaopnlem  24256  mbfinf  24266  itg1addlem4  24300  mbfi1fseqlem1  24316  mbfi1fseqlem3  24318  mbfi1fseqlem4  24319  mbfi1fseqlem5  24320  mbfi1fseqlem6  24321  itg2seq  24343  itg2lea  24345  itg2split  24350  itg2cnlem1  24362  limciun  24492  dvmptfsum  24572  rolle  24587  c1lip1  24594  dvcnvrelem1  24614  dvcnvre  24616  dvcvx  24617  itgsubst  24646  tdeglem4  24654  mdegmullem  24672  plyco0  24782  coemullem  24840  dgreq0  24855  dgrmul  24860  dgrco  24865  elqaalem2  24909  aannenlem1  24917  aaliou3lem9  24939  ulmres  24976  ulmshftlem  24977  angneg  25381  dcubic  25424  cxploglim  25555  cxploglim2  25556  scvxcvx  25563  lgamgulmlem5  25610  lgamcvg2  25632  ftalem2  25651  basellem3  25660  basellem4  25661  sqff1o  25759  fsumdvdsdiaglem  25760  dvdsflsumcom  25765  dvdsmulf1o  25771  fsumvma2  25790  logfac2  25793  logfacrlim  25800  logexprlim  25801  dchrelbasd  25815  lgsne0  25911  lgsqrlem2  25923  lgsqrmodndvds  25929  gausslemma2dlem1a  25941  lgseisenlem2  25952  lgsquadlem1  25956  lgsquadlem2  25957  lgsquadlem3  25958  lgsquad2lem2  25961  2sqlem8  26002  2sqlem11  26005  2sqreultlem  26023  2sqreunnltlem  26026  chpo1ubb  26057  vmadivsum  26058  rplogsumlem2  26061  rpvmasumlem  26063  dchrmusum2  26070  dchrvmasumlem1  26071  dchrisum0fno1  26087  dchrisum0re  26089  dchrisum0lem1  26092  dchrisum0lem2  26094  dchrisum0lem3  26095  dchrisum0  26096  mulogsumlem  26107  mulog2sumlem2  26111  vmalogdivsum2  26114  logsqvma  26118  log2sumbnd  26120  selberglem3  26123  selberg  26124  selberg2lem  26126  selberg2b  26128  selberg3lem2  26134  pntrmax  26140  pntrsumo1  26141  pntlemn  26176  pntlemp  26186  qabvle  26201  ostthlem1  26203  ostthlem2  26204  ostth2lem2  26210  ostth3  26214  idmot  26323  brbtwn2  26691  colinearalglem4  26695  colinearalg  26696  ax5seglem9  26723  axpaschlem  26726  axcontlem2  26751  axcontlem7  26756  axcontlem8  26757  eengtrkg  26772  upgr1eopALT  26902  uspgredg2vlem  27005  subumgr  27070  nbgr0vtxlem  27137  edgnbusgreu  27149  nb3grprlem1  27162  wlkl1loop  27419  pthdivtx  27510  usgr2pth  27545  crctcshwlkn0  27599  wlklnwwlkln1  27646  wwlksnext  27671  clwwlkccatlem  27767  clwlkclwwlklem2a  27776  clwwlkinwwlk  27818  clwwlkn1loopb  27821  clwwlkf  27826  wwlksext2clwwlk  27836  wwlksubclwwlk  27837  clwwlknscsh  27841  clwwlknon1  27876  clwwlknonex2e  27889  1conngr  27973  n4cyclfrgr  28070  numclwwlk2lem1lem  28121  2clwwlk2clwwlk  28129  numclwwlk1lem2f1  28136  numclwlk1lem1  28148  numclwwlk2lem1  28155  numclwlk2lem2f  28156  numclwwlk7  28170  frgrogt3nreg  28176  grpoidinvlem1  28281  grpoidinvlem3  28283  grporcan  28295  nmlnoubi  28573  blocnilem  28581  ipblnfi  28632  htthlem  28694  ocsh  29060  shmodsi  29166  pjhthlem2  29169  5oalem2  29432  eigposi  29613  nmopub2tALT  29686  nmfnleub2  29703  nmcexi  29803  nmopcoi  29872  kbass3  29895  mdslmd1lem1  30102  mdslmd1lem2  30103  chirredlem2  30168  chirredlem4  30170  mdsymlem3  30182  mdsymlem5  30184  sumdmdii  30192  sumdmdlem  30195  sumdmdlem2  30196  foresf1o  30265  disjxpin  30338  1stpreimas  30441  resf1o  30466  nn0xmulclb  30496  wrdt2ind  30627  xrge0tsmsd  30692  gsumvsca1  30854  gsumvsca2  30855  islinds5  30932  mdetpmtr1  31088  mdetpmtr2  31089  pstmxmet  31137  qqhghm  31229  qqhrhm  31230  esumpcvgval  31337  volmeas  31490  imambfm  31520  dya2iocnrect  31539  oddpwdc  31612  sseqf  31650  orvcgteel  31725  orvclteel  31730  ballotlemsf1o  31771  bnj1110  32254  bnj1118  32256  f1resveqaeq  32358  txpconn  32479  connpconn  32482  cnllysconn  32492  rellysconn  32498  cvmsss2  32521  cvmlift2lem9  32558  satf00  32621  fmlasuc  32633  mrsubfval  32755  mppsval  32819  dfon2lem6  33033  trpredmintr  33070  wzel  33111  fprlem1  33137  frrlem15  33142  sltres  33169  nosupno  33203  nosupbnd2  33216  sslttr  33268  ifscgr  33505  cgrxfr  33516  btwnconn1lem5  33552  btwnconn1lem6  33553  btwnconn1lem12  33559  brsegle  33569  finminlem  33666  nn0prpwlem  33670  fnessref  33705  refssfne  33706  neibastop1  33707  topjoin  33713  fnemeet2  33715  bj-prmoore  34410  bj-imdirid  34478  bj-finsumval0  34570  topdifinffinlem  34631  lindsadd  34900  matunitlindflem2  34904  poimirlem28  34935  poimirlem32  34939  opnmbllem0  34943  mblfinlem1  34944  mblfinlem4  34947  ismblfin  34948  mbfresfi  34953  itg2addnclem  34958  itg2addnclem3  34960  itg2addnc  34961  bddiblnc  34977  unirep  35003  frinfm  35025  sdclem2  35032  geomcau  35049  istotbnd3  35064  sstotbnd2  35067  sstotbnd  35068  sstotbnd3  35069  totbndbnd  35082  cntotbnd  35089  ismtyres  35101  heibor1lem  35102  heiborlem1  35104  heiborlem8  35111  ismndo1  35166  isdivrngo  35243  unichnidl  35324  erim2  35926  cvlcvr1  36490  ishlat3N  36505  llnmlplnN  36690  islvol2aN  36743  4atlem4c  36752  4atlem4d  36753  isline2  36925  isline3  36927  linepsubclN  37102  lhpexle3lem  37162  lhpjat2  37172  cdlemd4  37352  cdleme0cq  37366  cdleme32fva  37588  cdleme32fvaw  37590  tendo0mul  37977  tendo0mulr  37978  diameetN  38207  dvhvaddcl  38246  dvhvaddcomN  38247  cdlemm10N  38269  dvadiaN  38279  djavalN  38286  dihvalcqat  38390  dihopelvalcpre  38399  djhval  38549  dihjat1lem  38579  remul01  39257  prjspertr  39275  prjsprellsp  39281  elrfi  39311  nacsfix  39329  fzsplit1nn0  39371  eldioph2  39379  lzenom  39387  irrapxlem3  39441  pellexlem5  39450  pell1234qrne0  39470  pell1234qrmulcl  39472  pell14qrdich  39486  pell1qrge1  39487  pellqrex  39496  reglogltb  39508  reglogleb  39509  rmxypairf1o  39528  rmxycomplete  39534  monotoddzzfi  39559  congadd  39583  congsym  39585  acongrep  39597  jm2.19lem3  39608  jm2.19lem4  39609  jm2.22  39612  jm2.25  39616  expdiophlem1  39638  wepwsolem  39662  kelac1  39683  lmhmfgsplit  39706  pwslnm  39714  hbtlem6  39749  hbt  39750  mon1psubm  39826  deg1mhm  39827  iunrelexp0  40067  dssmapnvod  40386  gsumws3  40569  gsumws4  40570  mulltgt0  41299  fnchoice  41306  disjrnmpt2  41469  fzisoeu  41587  fsumiunss  41876  climinf  41907  mullimc  41917  mullimcf  41924  stoweidlem14  42319  stoweidlem17  42322  stoweidlem34  42339  stoweidlem50  42355  fourierdlem42  42454  fourierdlem62  42473  fourierdlem71  42482  fourierdlem76  42487  qndenserrnbllem  42599  subsaliuncl  42661  sge0resplit  42708  2reu8i  43332  fundcmpsurinjpreimafv  43588  iccpartigtl  43603  prproropf1olem2  43686  prproropf1olem4  43688  paireqne  43693  prmdvdsfmtnof1lem2  43767  bgoldbtbndlem3  43992  bgoldbtbnd  43994  isomushgr  44011  isomuspgrlem2c  44015  uspgrsprf1  44042  subsubmgm  44084  isassintop  44137  2zlidl  44225  2zrngnmrid  44241  rngcinv  44272  rngcinvALTV  44284  ringcinv  44323  funcringcsetcALTV2lem9  44335  ringcinvALTV  44347  funcringcsetclem9ALTV  44358  fldhmsubc  44375  fldhmsubcALTV  44393  mndpsuppss  44439  gsumlsscl  44451  lincsum  44504  lindslinindsimp1  44532  lindslinindimp2lem4  44536  lincresunitlem2  44551  elfzolborelfzop1  44594  elbigo2  44632  digexp  44687  dig1  44688  nn0sumshdiglemB  44700  itschlc0xyqsol  44774