Theorem adantrl 717

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrl	⊢ ((𝜑 ∧ (𝜃 ∧ 𝜓)) → 𝜒)

Proof of Theorem adantrl

Step	Hyp	Ref	Expression
1		simpr 484	. 2 ⊢ ((𝜃 ∧ 𝜓) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 594	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:  ad2ant2l  747  ad2ant2rl  750  cases2ALT  1049  consensus  1053  3ad2antr2  1191  3ad2antr3  1192  po2ne  5556  opabssxpd  5679  frpoind  6308  ordelord  6347  f1un  6802  fvelima2  6894  f1cofveqaeqALT  7214  isocnv  7286  isores2  7289  f1oiso2  7308  offval  7641  ordsucun  7777  xp2nd  7976  2ndconst  8053  sexp2  8098  smoord  8307  tfrlem9  8326  tfrlem11  8329  oaass  8498  omordi  8503  omwordri  8509  odi  8516  oewordri  8530  nnawordi  8559  nnmordi  8569  coflton  8609  dom2lem  8941  fundmen  8980  sbthlem9  9035  mapen  9081  mapunen  9086  ssenen  9091  domfi  9125  mapfien  9323  inf3lem6  9554  ttrclselem2  9647  frind  9674  r1val1  9710  rankval3b  9750  numacn  9971  infxpabs  10133  infxp  10136  cfsmolem  10192  infpssrlem4  10228  fin23lem27  10250  isf34lem4  10299  hsmexlem2  10349  axdc3lem2  10373  axdc3lem4  10375  iundom2g  10462  gchen1  10548  fpwwe2lem6  10559  fpwwe2lem10  10563  fpwwe2lem11  10564  prlem936  10970  muladd  11581  leord1  11676  eqord1  11677  ltord2  11678  leord2  11679  eqord2  11680  divadddiv  11868  ltmul12a  12009  lemul12b  12010  fimaxre  12098  supadd  12122  supmullem1  12124  cju  12153  zextlt  12578  zmax  12870  xrre  13096  supxr  13240  ixxdisj  13288  iooshf  13354  icodisj  13404  ioojoin  13411  iccshftr  13414  iccshftl  13416  iccdil  13418  icccntr  13420  iccf1o  13424  fzaddel  13486  fzsubel  13488  modadd1  13840  modmul1  13859  seqcaopr  13974  expsub  14045  expmordi  14102  sqlecan  14144  facndiv  14223  hashss  14344  hashfacen  14389  hashf1lem1  14390  fi1uzind  14442  brfi1indALT  14445  ccatpfx  14636  swrdccatfn  14659  swrdccatin2  14664  2cshwcshw  14760  resqrex  15185  fprodeq0  15910  lcmdvds  16547  hashdvds  16714  eulerthlem2  16721  pceu  16786  pcqcl  16796  infpnlem1  16850  4sqlem11  16895  ramcl  16969  prmgaplem5  16995  imasvscafn  17470  invfun  17700  initoeu2lem2  17951  catcisolem  18046  funcestrcsetclem8  18082  fullestrcsetc  18086  embedsetcestrclem  18092  funcsetcestrclem8  18097  fullsetcestrc  18101  prfcl  18138  prf1st  18139  prf2nd  18140  1st2ndprf  18141  curfuncf  18173  ipodrsfi  18474  mgmhmpropd  18635  subsubmgm  18647  mhmpropd  18729  subsubm  18753  pwsdiagmhm  18768  frmdgsum  18799  grplcan  18942  grplmulf1o  18955  grpraddf1o  18956  dfgrp3lem  18980  mulgsubcl  19030  subsubg  19091  eqger  19119  qus0subgadd  19140  resghm  19173  conjghm  19190  orbsta  19254  psgnunilem2  19436  odmulg  19497  sylow2a  19560  sylow3lem1  19568  lsmssv  19584  pj1ghm  19644  frgpup1  19716  ghmplusg  19787  subsubrng  20508  subsubrg  20543  srhmsubc  20625  issrngd  20800  lmhmco  21007  lmhmf1o  21010  lmhmima  21011  lmhmpreima  21012  reslmhm  21016  pwsdiaglmhm  21021  pwssplit2  21024  pwssplit3  21025  pj1lmhm  21064  lspdisj  21092  rngqiprngghmlem2  21255  rngqiprngghm  21266  prmirred  21441  cygznlem3  21536  frlmsslsp  21763  frlmlbs  21764  frlmup1  21765  issubassa2  21860  psrbagconf1o  21897  psrgrp  21924  evlslem2  22046  evlslem1  22049  evlsvvval  22060  ply1sclf1  22243  mamuass  22358  dmatmul  22453  dmatsubcl  22454  dmatmulcl  22456  dmatcrng  22458  scmatcrng  22477  mdetunilem9  22576  pm2mpghm  22772  fvmptnn04ifb  22807  toponmre  23049  neiptopreu  23089  ordtbas  23148  txcls  23560  txlm  23604  qtoptop2  23655  qtoprest  23673  kqt0lem  23692  ptuncnv  23763  fmfnfmlem4  23913  alexsubALTlem2  24004  tgpmulg  24049  blin  24377  xmeter  24389  xmetresbl  24393  dscmet  24528  nmdvr  24626  metnrmlem3  24818  icccvx  24916  bndth  24925  htpycc  24947  pcohtpylem  24987  pi1blem  25007  lmmbrf  25230  iscfil2  25234  iscau4  25247  minveclem7  25403  elovolm  25444  dyaddisjlem  25564  ismbfd  25608  itg1mulc  25673  dvlip  25966  dvcvx  25993  plypf1  26185  eff1olem  26525  logccv  26640  lawcos  26794  leibpilem1  26918  sqff1o  27160  dvdsppwf1o  27164  dvdsflf1o  27165  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  sgmmul  27180  fsumvma  27192  bposlem6  27268  lgsdchr  27334  rpvmasum2  27491  pntpbnd1  27565  ostthlem1  27606  ltsres  27642  nodenselem5  27668  nodenselem6  27669  nodense  27672  addsproplem2  27978  mulsuniflem  28157  mulsunif2lem  28177  precsexlem9  28223  precsexlem10  28224  precsexlem11  28225  om2noseqlt2  28308  om2noseqf1o  28309  z12sge0  28491  elreno2  28503  tgbtwntriv2  28571  ercgrg  28601  hlpasch  28840  colinearalglem4  28994  axlowdimlem15  29041  axcontlem7  29055  axcontlem8  29056  axcontlem10  29058  usgr1v  29341  pthdivtx  29812  clwwlkn1loopb  30130  grpolcan  30618  nvmf  30733  sspmval  30821  nmosetre  30852  minvecolem7  30971  hiassdi  31179  shscli  31405  fh1  31706  fh2  31707  cm2j  31708  chscllem2  31726  spansncvi  31740  5oalem2  31743  adjsym  31921  nmopsetretALT  31951  nmfnsetre  31965  cnvadj  31980  cnvunop  32006  unoplin  32008  hmoplin  32030  lnopmi  32088  hmops  32108  hmopm  32109  nmcexi  32114  adjlnop  32174  adjmul  32180  adjadd  32181  opsqrlem1  32228  mdsl0  32398  ssmd2  32400  mdexchi  32423  superpos  32442  chrelat2i  32453  atcvatlem  32473  atcvati  32474  chirredlem1  32478  chirredi  32482  atcvat3i  32484  atcvat4i  32485  mdsymlem3  32493  mdsymlem5  32495  cdj3lem2b  32525  ifnebib  32636  isoun  32792  xrge0infss  32851  1arithufdlem3  33639  extdg1id  33844  ddemeas  34414  fsum2dsub  34785  hgt750lemb  34834  bnj1145  35169  subfacp1lem3  35398  subfacp1lem5  35400  cvxpconn  35458  satfv1lem  35578  btwnconn1lem12  36314  colinbtwnle  36334  broutsideof2  36338  lineelsb2  36364  nn0prpwlem  36538  neibastop2lem  36576  tailfb  36593  onsuct0  36657  finxpreclem2  37645  lindsenlbs  37866  poimirlem4  37875  poimirlem26  37897  poimirlem27  37898  poimirlem31  37902  heicant  37906  mblfinlem2  37909  mblfinlem3  37910  ismblfin  37912  ftc1anclem5  37948  ftc1anclem6  37949  ftc1anc  37952  sdclem1  37994  seqpo  37998  sstotbnd  38026  cntotbnd  38047  ismtycnv  38053  ismtyres  38059  heibor  38072  exidreslem  38128  ghomdiv  38143  grpokerinj  38144  rngohomco  38225  rngoisoco  38233  idlsubcl  38274  divrngidl  38279  ispridl2  38289  ispridlc  38321  riotasv3d  39336  omllaw3  39621  omlfh1N  39634  hlrelat2  39779  cvratlem  39797  cvrat  39798  cvrat3  39818  cvrat4  39819  ps-2  39854  elpaddn0  40176  paddss12  40195  pmodlem2  40223  cdleme0cq  40591  cdlemeg49lebilem  40915  cdleme50eq  40917  tendoeq2  41150  tendoex  41351  diameetN  41432  diainN  41433  dvhopN  41492  djajN  41513  dihmeetcl  41721  mapdheq2  42105  3factsumint1  42391  imacrhmcl  42884  psrmnd  42913  evlselvlem  42944  fsuppind  42948  0prjspn  42986  fphpdo  43174  pell1234qrne0  43210  pell14qrgt0  43216  pell1qrge1  43227  monotoddzzfi  43299  jm2.18  43345  wepwsolem  43399  dnnumch3  43404  dnwech  43405  kelac1  43420  kercvrlsm  43440  onov0suclim  43631  cantnfresb  43681  dssmapnvod  44376  gsumws3  44552  gsumws4  44553  mnuprdlem1  44628  mnuprdlem2  44629  traxext  45333  modelac8prim  45348  cncmpmax  45392  fiiuncl  45425  choicefi  45558  mullimc  45976  mullimcf  45983  idlimc  45986  limclner  46009  climleltrp  46034  limsupub  46062  climuzlem  46101  climliminflimsup2  46167  xlimbr  46185  xlimxrre  46189  dfxlim2v  46205  fperdvper  46277  ioodvbdlimc1lem2  46290  ioodvbdlimc2lem  46292  dvnprodlem1  46304  stoweidlem27  46385  stoweidlem48  46406  fourierdlem42  46507  fourierdlem63  46527  fourierdlem65  46529  dfsalgen2  46699  subsaliuncl  46716  sge0iunmptlemfi  46771  sge0rpcpnf  46779  iundjiun  46818  psmeasure  46829  ovnsubaddlem2  46929  hoidmvle  46958  ovolval4lem2  47008  smflimlem2  47130  smflimlem3  47131  smflimlem6  47134  smflimmpt  47168  fcoresf1  47429  icceuelpart  47796  gpgedgvtx0  48421  gpgedgvtx1  48422  srhmsubcALTV  48685  catprs  49370  thincciso2  49814  functermclem  49866  functermc  49867  fulltermc  49870