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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  simprl  771  simprll  779  simprlr  780  simprl1  1220  simprl2  1221  simprl3  1222  disjxiun  5036  reusv2lem4  5279  axprlem5  5305  fr2nr  5514  somin1  5978  tz7.7  6217  f1oprg  6683  soisores  7114  elovmporab1w  7430  elovmporab1  7431  sorpssi  7495  onint  7552  ordsucelsuc  7579  elxp5  7679  wemoiso  7724  wemoiso2  7725  el2xptp0  7786  ressuppss  7903  fprlem1  8019  tz7.48lem  8155  oalimcl  8266  oeeui  8308  oaabs2  8352  omabs  8354  swoer  8399  ralxpmap  8555  pw2f1olem  8727  enfixsn  8732  mapxpen  8790  mapunen  8793  unxpdomlem2  8859  unxpdomlem3  8860  findcard3  8892  isfinite2  8907  domunfican  8922  fodomfi  8927  fissuni  8959  fipreima  8960  indexfi  8962  fsuppsssupp  8979  marypha1lem  9027  marypha2  9033  supmo  9046  infmo  9089  oieu  9133  brwdom2  9167  ixpiunwdom  9184  cantnfval2  9262  cantnfle  9264  cantnflt  9265  cantnf  9286  wemapwe  9290  cnfcom  9293  trpredmintr  9314  rankonidlem  9409  r1pwcl  9428  eldju2ndl  9505  eldju2ndr  9506  djuun  9507  infxpenlem  9592  infxpenc2lem1  9598  fseqenlem1  9603  dfac8clem  9611  mappwen  9691  dfac3  9700  dfac5  9707  dfac12lem3  9724  infunsdom  9793  coftr  9852  ssfin4  9889  domfin4  9890  fin23lem26  9904  fin23lem22  9906  fin23lem28  9919  fin23lem32  9923  fin23lem40  9930  isf32lem5  9936  compssiso  9953  isf34lem4  9956  isfin1-3  9965  fin1a2lem13  9991  hsmexlem2  10006  hsmexlem4  10008  zorn2lem1  10075  ttukeylem6  10093  iundom2g  10119  konigthlem  10147  pwcfsdom  10162  fpwwe2lem11  10220  fpwwe2  10222  pwfseqlem3  10239  winalim2  10275  r1wunlim  10316  inttsk  10353  inar1  10354  grur1  10399  nqereq  10514  ltexprlem7  10621  prlem936  10626  00id  10972  addid2  10980  ltord1  11323  divdiv1  11508  divdiv2  11509  conjmul  11514  ltdivmul  11672  ledivmul  11673  lt2mul2div  11675  ltdiv23  11688  lediv23  11689  lediv12a  11690  ledivp1  11699  negfi  11746  nn0nndivcl  12126  nn0ge0div  12211  peano2uz2  12230  peano5uzi  12231  eluzp1m1  12429  qbtwnre  12754  xralrple  12760  xleadd1a  12808  xmulge0  12839  xmulass  12842  xlemul1a  12843  iooshf  12979  divelunit  13047  eluzgtdifelfzo  13269  modadd1  13446  modmul1  13462  seqcl2  13559  seqfveq2  13563  seqid2  13587  seqhomo  13588  seqdistr  13592  mulexpz  13640  leexp2r  13709  expnlbnd2  13766  expmulnbnd  13767  hashmap  13967  hashfun  13969  hashbclem  13981  hashfacen  13983  hashfacenOLD  13984  hashf1lem2  13987  hashf1  13988  ccatsymb  14104  swrdwrdsymb  14192  swrdsb0eq  14193  ccatpfx  14231  swrdswrd  14235  wrdind  14252  wrd2ind  14253  swrdccatin1  14255  swrdccatin2  14259  pfxccatin12lem2  14261  pfxccatin12  14263  swrdccat  14265  repswswrd  14314  0csh0  14323  cshwidxmod  14333  2cshw  14343  cshweqrep  14351  relexp0g  14550  relexpsucnnr  14553  relexpindlem  14591  sqrlem1  14771  sqrlem6  14776  rlim  15021  rlimclim1  15071  climsup  15198  caurcvg2  15206  caucvgb  15208  iseralt  15213  sumss  15253  fsum2dlem  15297  mptfzshft  15305  modfsummod  15321  o1fsum  15340  incexclem  15363  divrcnv  15379  flo1  15381  fprodrev  15502  fprod2dlem  15505  ruclem6  15759  moddvds  15789  dvdsaddre2b  15831  dvdsflip  15841  addmodlteqALT  15849  nn0o  15907  fldivndvdslt  15938  bitsf1ocnv  15966  bitsf1  15968  sadcaddlem  15979  bezoutlem2  16063  bezoutlem4  16065  lcmgcdlem  16126  prmind2  16205  isprm5  16227  isprm6  16234  prmdvdsncoprmbd  16246  cncongrprm  16248  hashdvds  16291  crth  16294  eulerthlem2  16298  prmdiveq  16302  hashgcdlem  16304  hashgcdeq  16305  iserodd  16351  pclem  16354  pcprendvds2  16357  pcexp  16375  pcneg  16390  pc2dvds  16395  pcmpt  16408  prmpwdvds  16420  pockthg  16422  prmreclem5  16436  4sqlem11  16471  ramub2  16530  ramubcl  16534  ram0  16538  ramub1lem2  16543  ramcl  16545  prmgaplem3  16569  prmgaplem6  16572  setscom  16709  sscpwex  17274  initoeu2  17476  setcinv  17550  funcestrcsetclem9  17609  funcsetcestrclem9  17624  fullsetcestrc  17627  1stfcl  17658  2ndfcl  17659  hofpropd  17729  isacs3lem  18002  isacs4lem  18004  acsmap2d  18015  submnd0  18156  subsubm  18197  insubm  18199  frmdup1  18245  frmdup3lem  18247  sgrp2nmndlem2  18305  isgrpinv  18374  subsubg  18520  cycsubgcl  18567  conjghm  18607  qusghm  18613  gsumwrev  18712  gsmsymgrfixlem1  18773  symgfixelsi  18781  symgsssg  18813  symgfisg  18814  psgnunilem2  18841  odf1o2  18916  sylow1lem1  18941  odcau  18947  pgpfi  18948  pgpssslw  18957  fislw  18968  efgtlen  19070  efginvrel2  19071  efgrelexlemb  19094  efgredeu  19096  efgcpbllemb  19099  frgpup1  19119  cygablOLD  19230  lt6abl  19234  gsum2d  19311  gsum2d2lem  19312  gsum2d2  19313  telgsumfzslem  19327  dmdprdsplit2lem  19386  ablfacrp  19407  pgpfac1lem3  19418  gsummgp0  19580  irredrmul  19679  subsubrg  19780  islss4  19953  lspextmo  20047  lspsnat  20136  prmirredlem  20413  znf1o  20470  znidomb  20480  frgpcyg  20492  psgnghm  20496  psgndiflemB  20516  frlmlbs  20713  frlmup1  20714  lindfind  20732  islindf3  20742  lindfmm  20743  issubassa3  20781  resspsradd  20895  resspsrmul  20896  coe1tmmul2  21151  pf1ind  21225  mamulid  21292  mat1dimelbas  21322  mdetdiaglem  21449  mdetralt2  21460  mndifsplit  21487  smadiadetglem2  21523  1elcpmat  21566  pmatcollpw3lem  21634  chfacfisf  21705  chfacfisfcpmat  21706  chfacffsupp  21707  chfacfscmulfsupp  21710  chfacfscmulgsum  21711  chfacfpmmulfsupp  21714  chfacfpmmulgsum  21715  chfacfpmmulgsum2  21716  cayhamlem1  21717  cpmadugsumlemF  21727  cayleyhamilton1  21743  tgcl  21820  pptbas  21859  clsval2  21901  mretopd  21943  lmbr2  22110  cncls2  22124  nrmsep  22208  regsep2  22227  cmpsublem  22250  cmpsub  22251  tgcmp  22252  uncmp  22254  hauscmplem  22257  iunconnlem  22278  1stcrest  22304  2ndcctbss  22306  2ndcsep  22310  dis2ndc  22311  hausllycmp  22345  dislly  22348  kgentopon  22389  1stckgen  22405  kgencn3  22409  ptpjpre1  22422  ptbasin  22428  ptpjopn  22463  dfac14  22469  ptcnplem  22472  txcn  22477  txindis  22485  txdis1cn  22486  ptrescn  22490  txcmplem1  22492  txcmp  22494  txhaus  22498  txlm  22499  tx1stc  22501  txkgen  22503  xkococn  22511  qtopcn  22565  kqreglem1  22592  kqreglem2  22593  kqnrmlem1  22594  kqnrmlem2  22595  hmeoimaf1o  22621  reghmph  22644  nrmhmph  22645  txhmeo  22654  ptuncnv  22658  filconn  22734  fbasrn  22735  fmfnfmlem2  22806  flimfnfcls  22879  cnpfcfi  22891  alexsublem  22895  alexsubALTlem2  22899  alexsubALTlem3  22900  alexsubALTlem4  22901  alexsubALT  22902  ptcmplem3  22905  cnextfval  22913  tsmsxp  23006  imasdsf1olem  23225  bl2in  23252  blssps  23276  blss  23277  blssexps  23278  blssex  23279  blcld  23357  stdbdxmet  23367  met1stc  23373  prdsxmslem2  23381  metcnp3  23392  metcnpi3  23398  txmetcnp  23399  nmo0  23587  nmoid  23594  icccmplem1  23673  icccmp  23676  xrge0tsms  23685  metdseq0  23705  cnheiborlem  23805  cnheibor  23806  cnllycmp  23807  pcoval2  23867  cmetcaulem  24139  iscmet3lem1  24142  iscmet3lem2  24143  equivcau  24151  lmcau  24164  cncmet  24173  ivthlem2  24303  ivthlem3  24304  ovoliunlem2  24354  ovolscalem2  24365  uniioombl  24440  dyaddisj  24447  opnmbllem  24452  volivth  24458  ismbfd  24490  ismbf3d  24505  mbfimaopnlem  24506  mbfinf  24516  itg1addlem4  24550  itg1addlem4OLD  24551  mbfi1fseqlem1  24567  mbfi1fseqlem3  24569  mbfi1fseqlem4  24570  mbfi1fseqlem5  24571  mbfi1fseqlem6  24572  itg2seq  24594  itg2lea  24596  itg2split  24601  itg2cnlem1  24613  bddiblnc  24693  limciun  24745  dvmptfsum  24826  rolle  24841  c1lip1  24848  dvcnvrelem1  24868  dvcnvre  24870  dvcvx  24871  itgsubst  24900  tdeglem4  24911  tdeglem4OLD  24912  mdegmullem  24930  plyco0  25040  coemullem  25098  dgreq0  25113  dgrmul  25118  dgrco  25123  elqaalem2  25167  aannenlem1  25175  aaliou3lem9  25197  ulmres  25234  ulmshftlem  25235  angneg  25640  dcubic  25683  cxploglim  25814  cxploglim2  25815  scvxcvx  25822  lgamgulmlem5  25869  lgamcvg2  25891  ftalem2  25910  basellem3  25919  basellem4  25920  sqff1o  26018  fsumdvdsdiaglem  26019  dvdsflsumcom  26024  dvdsmulf1o  26030  fsumvma2  26049  logfac2  26052  logfacrlim  26059  logexprlim  26060  dchrelbasd  26074  lgsne0  26170  lgsqrlem2  26182  lgsqrmodndvds  26188  gausslemma2dlem1a  26200  lgseisenlem2  26211  lgsquadlem1  26215  lgsquadlem2  26216  lgsquadlem3  26217  lgsquad2lem2  26220  2sqlem8  26261  2sqlem11  26264  2sqreultlem  26282  2sqreunnltlem  26285  chpo1ubb  26316  vmadivsum  26317  rplogsumlem2  26320  rpvmasumlem  26322  dchrmusum2  26329  dchrvmasumlem1  26330  dchrisum0fno1  26346  dchrisum0re  26348  dchrisum0lem1  26351  dchrisum0lem2  26353  dchrisum0lem3  26354  dchrisum0  26355  mulogsumlem  26366  mulog2sumlem2  26370  vmalogdivsum2  26373  logsqvma  26377  log2sumbnd  26379  selberglem3  26382  selberg  26383  selberg2lem  26385  selberg2b  26387  selberg3lem2  26393  pntrmax  26399  pntrsumo1  26400  pntlemn  26435  pntlemp  26445  qabvle  26460  ostthlem1  26462  ostthlem2  26463  ostth2lem2  26469  ostth3  26473  idmot  26582  brbtwn2  26950  colinearalglem4  26954  colinearalg  26955  ax5seglem9  26982  axpaschlem  26985  axcontlem2  27010  axcontlem7  27015  axcontlem8  27016  eengtrkg  27031  upgr1eopALT  27162  uspgredg2vlem  27265  subumgr  27330  nbgr0vtxlem  27397  edgnbusgreu  27409  nb3grprlem1  27422  wlkl1loop  27679  pthdivtx  27770  usgr2pth  27805  crctcshwlkn0  27859  wlklnwwlkln1  27906  wwlksnext  27931  clwwlkccatlem  28026  clwlkclwwlklem2a  28035  clwwlkinwwlk  28077  clwwlkn1loopb  28080  clwwlkf  28084  wwlksext2clwwlk  28094  wwlksubclwwlk  28095  clwwlknscsh  28099  clwwlknon1  28134  clwwlknonex2e  28147  1conngr  28231  n4cyclfrgr  28328  numclwwlk2lem1lem  28379  2clwwlk2clwwlk  28387  numclwwlk1lem2f1  28394  numclwlk1lem1  28406  numclwwlk2lem1  28413  numclwlk2lem2f  28414  numclwwlk7  28428  frgrogt3nreg  28434  grpoidinvlem1  28539  grpoidinvlem3  28541  grporcan  28553  nmlnoubi  28831  blocnilem  28839  ipblnfi  28890  htthlem  28952  ocsh  29318  shmodsi  29424  pjhthlem2  29427  5oalem2  29690  eigposi  29871  nmopub2tALT  29944  nmfnleub2  29961  nmcexi  30061  nmopcoi  30130  kbass3  30153  mdslmd1lem1  30360  mdslmd1lem2  30361  chirredlem2  30426  chirredlem4  30428  mdsymlem3  30440  mdsymlem5  30442  sumdmdii  30450  sumdmdlem  30453  sumdmdlem2  30454  foresf1o  30523  disjxpin  30600  1stpreimas  30712  resf1o  30739  nn0xmulclb  30768  wrdt2ind  30899  xrge0tsmsd  30990  gsumvsca1  31152  gsumvsca2  31153  islinds5  31231  mdetpmtr1  31441  mdetpmtr2  31442  pstmxmet  31515  qqhghm  31604  qqhrhm  31605  esumpcvgval  31712  volmeas  31865  imambfm  31895  dya2iocnrect  31914  oddpwdc  31987  sseqf  32025  orvcgteel  32100  orvclteel  32105  ballotlemsf1o  32146  bnj1110  32629  bnj1118  32631  f1resveqaeq  32724  txpconn  32861  connpconn  32864  cnllysconn  32874  rellysconn  32880  cvmsss2  32903  cvmlift2lem9  32940  satf00  33003  fmlasuc  33015  mrsubfval  33137  mppsval  33201  dfon2lem6  33434  frxp2  33471  poxp3  33476  frxp3  33477  wzel  33498  frrlem15  33505  sltres  33551  nosupno  33592  nosupbnd2  33605  noinfno  33607  noinfbnd2  33620  etasslt  33693  ifscgr  34032  cgrxfr  34043  btwnconn1lem5  34079  btwnconn1lem6  34080  btwnconn1lem12  34086  brsegle  34096  finminlem  34193  nn0prpwlem  34197  fnessref  34232  refssfne  34233  neibastop1  34234  topjoin  34240  fnemeet2  34242  bj-prmoore  34970  bj-finsumval0  35140  topdifinffinlem  35204  lindsadd  35456  matunitlindflem2  35460  poimirlem28  35491  poimirlem32  35495  opnmbllem0  35499  mblfinlem1  35500  mblfinlem4  35503  ismblfin  35504  mbfresfi  35509  itg2addnclem  35514  itg2addnclem3  35516  itg2addnc  35517  unirep  35557  frinfm  35579  sdclem2  35586  geomcau  35603  istotbnd3  35615  sstotbnd2  35618  sstotbnd  35619  sstotbnd3  35620  totbndbnd  35633  cntotbnd  35640  ismtyres  35652  heibor1lem  35653  heiborlem1  35655  heiborlem8  35662  ismndo1  35717  isdivrngo  35794  unichnidl  35875  erim2  36475  cvlcvr1  37039  ishlat3N  37054  llnmlplnN  37239  islvol2aN  37292  4atlem4c  37301  4atlem4d  37302  isline2  37474  isline3  37476  linepsubclN  37651  lhpexle3lem  37711  lhpjat2  37721  cdlemd4  37901  cdleme0cq  37915  cdleme32fva  38137  cdleme32fvaw  38139  tendo0mul  38526  tendo0mulr  38527  diameetN  38756  dvhvaddcl  38795  dvhvaddcomN  38796  cdlemm10N  38818  dvadiaN  38828  djavalN  38835  dihvalcqat  38939  dihopelvalcpre  38948  djhval  39098  dihjat1lem  39128  sticksstones11  39781  metakunt15  39802  metakunt16  39803  evlsbagval  39926  fsuppind  39930  mhpind  39934  mhphf  39936  remul01  40039  prjspertr  40093  prjsprellsp  40099  elrfi  40160  nacsfix  40178  fzsplit1nn0  40220  eldioph2  40228  lzenom  40236  irrapxlem3  40290  pellexlem5  40299  pell1234qrne0  40319  pell1234qrmulcl  40321  pell14qrdich  40335  pell1qrge1  40336  pellqrex  40345  reglogltb  40357  reglogleb  40358  rmxypairf1o  40377  rmxycomplete  40383  monotoddzzfi  40408  congadd  40432  congsym  40434  acongrep  40446  jm2.19lem3  40457  jm2.19lem4  40458  jm2.22  40461  jm2.25  40465  expdiophlem1  40487  wepwsolem  40511  kelac1  40532  lmhmfgsplit  40555  pwslnm  40563  hbtlem6  40598  hbt  40599  mon1psubm  40675  deg1mhm  40676  iunrelexp0  40928  dssmapnvod  41246  gsumws3  41426  gsumws4  41427  mulltgt0  42179  fnchoice  42186  disjrnmpt2  42340  fzisoeu  42453  fsumiunss  42734  climinf  42765  mullimc  42775  mullimcf  42782  stoweidlem14  43173  stoweidlem17  43176  stoweidlem34  43193  stoweidlem50  43209  fourierdlem42  43308  fourierdlem62  43327  fourierdlem71  43336  fourierdlem76  43341  qndenserrnbllem  43453  subsaliuncl  43515  sge0resplit  43562  2reu8i  44220  fundcmpsurinjpreimafv  44476  iccpartigtl  44491  prproropf1olem2  44572  prproropf1olem4  44574  paireqne  44579  prmdvdsfmtnof1lem2  44653  bgoldbtbndlem3  44875  bgoldbtbnd  44877  isomushgr  44894  isomuspgrlem2c  44898  uspgrsprf1  44925  subsubmgm  44967  isassintop  45020  2zlidl  45108  2zrngnmrid  45124  rngcinv  45155  rngcinvALTV  45167  ringcinv  45206  funcringcsetcALTV2lem9  45218  ringcinvALTV  45230  funcringcsetclem9ALTV  45241  fldhmsubc  45258  fldhmsubcALTV  45276  mndpsuppss  45323  gsumlsscl  45335  lincsum  45386  lindslinindsimp1  45414  lindslinindimp2lem4  45418  lincresunitlem2  45433  elfzolborelfzop1  45476  elbigo2  45514  digexp  45569  dig1  45570  nn0sumshdiglemB  45582  1arymaptf1  45604  2arymaptf1  45615  itcoval1  45625  itcoval2  45626  itcoval3  45627  itcovalsucov  45630  ackvalsuc1mpt  45640  itschlc0xyqsol  45729  thincciso  45946  indthinc  45949  indthincALT  45950