Theorem adantrl 716

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 593	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  746  ad2ant2rl  749  cases2ALT  1048  consensus  1052  3ad2antr2  1190  3ad2antr3  1191  po2ne  5545  opabssxpd  5668  frpoind  6297  ordelord  6336  f1un  6791  fvelima2  6883  f1cofveqaeqALT  7201  isocnv  7273  isores2  7276  f1oiso2  7295  offval  7628  ordsucun  7764  xp2nd  7963  2ndconst  8040  sexp2  8085  smoord  8294  tfrlem9  8313  tfrlem11  8316  oaass  8485  omordi  8490  omwordri  8496  odi  8503  oewordri  8516  nnawordi  8545  nnmordi  8555  coflton  8595  dom2lem  8925  fundmen  8964  sbthlem9  9019  mapen  9065  mapunen  9070  ssenen  9075  domfi  9109  mapfien  9303  inf3lem6  9534  ttrclselem2  9627  frind  9654  r1val1  9690  rankval3b  9730  numacn  9951  infxpabs  10113  infxp  10116  cfsmolem  10172  infpssrlem4  10208  fin23lem27  10230  isf34lem4  10279  hsmexlem2  10329  axdc3lem2  10353  axdc3lem4  10355  iundom2g  10442  gchen1  10527  fpwwe2lem6  10538  fpwwe2lem10  10542  fpwwe2lem11  10543  prlem936  10949  muladd  11560  leord1  11655  eqord1  11656  ltord2  11657  leord2  11658  eqord2  11659  divadddiv  11847  ltmul12a  11988  lemul12b  11989  fimaxre  12077  supadd  12101  supmullem1  12103  cju  12132  zextlt  12557  zmax  12849  xrre  13075  supxr  13219  ixxdisj  13267  iooshf  13333  icodisj  13383  ioojoin  13390  iccshftr  13393  iccshftl  13395  iccdil  13397  icccntr  13399  iccf1o  13403  fzaddel  13465  fzsubel  13467  modadd1  13819  modmul1  13838  seqcaopr  13953  expsub  14024  expmordi  14081  sqlecan  14123  facndiv  14202  hashss  14323  hashfacen  14368  hashf1lem1  14369  fi1uzind  14421  brfi1indALT  14424  ccatpfx  14615  swrdccatfn  14638  swrdccatin2  14643  2cshwcshw  14739  resqrex  15164  fprodeq0  15889  lcmdvds  16526  hashdvds  16693  eulerthlem2  16700  pceu  16765  pcqcl  16775  infpnlem1  16829  4sqlem11  16874  ramcl  16948  prmgaplem5  16974  imasvscafn  17449  invfun  17679  initoeu2lem2  17930  catcisolem  18025  funcestrcsetclem8  18061  fullestrcsetc  18065  embedsetcestrclem  18071  funcsetcestrclem8  18076  fullsetcestrc  18080  prfcl  18117  prf1st  18118  prf2nd  18119  1st2ndprf  18120  curfuncf  18152  ipodrsfi  18453  mgmhmpropd  18614  subsubmgm  18626  mhmpropd  18708  subsubm  18732  pwsdiagmhm  18747  frmdgsum  18778  grplcan  18921  grplmulf1o  18934  grpraddf1o  18935  dfgrp3lem  18959  mulgsubcl  19009  subsubg  19070  eqger  19098  qus0subgadd  19119  resghm  19152  conjghm  19169  orbsta  19233  psgnunilem2  19415  odmulg  19476  sylow2a  19539  sylow3lem1  19547  lsmssv  19563  pj1ghm  19623  frgpup1  19695  ghmplusg  19766  subsubrng  20487  subsubrg  20522  srhmsubc  20604  issrngd  20779  lmhmco  20986  lmhmf1o  20989  lmhmima  20990  lmhmpreima  20991  reslmhm  20995  pwsdiaglmhm  21000  pwssplit2  21003  pwssplit3  21004  pj1lmhm  21043  lspdisj  21071  rngqiprngghmlem2  21234  rngqiprngghm  21245  prmirred  21420  cygznlem3  21515  frlmsslsp  21742  frlmlbs  21743  frlmup1  21744  issubassa2  21839  psrbagconf1o  21876  psrgrp  21903  evlslem2  22025  evlslem1  22028  evlsvvval  22039  ply1sclf1  22222  mamuass  22337  dmatmul  22432  dmatsubcl  22433  dmatmulcl  22435  dmatcrng  22437  scmatcrng  22456  mdetunilem9  22555  pm2mpghm  22751  fvmptnn04ifb  22786  toponmre  23028  neiptopreu  23068  ordtbas  23127  txcls  23539  txlm  23583  qtoptop2  23634  qtoprest  23652  kqt0lem  23671  ptuncnv  23742  fmfnfmlem4  23892  alexsubALTlem2  23983  tgpmulg  24028  blin  24356  xmeter  24368  xmetresbl  24372  dscmet  24507  nmdvr  24605  metnrmlem3  24797  icccvx  24895  bndth  24904  htpycc  24926  pcohtpylem  24966  pi1blem  24986  lmmbrf  25209  iscfil2  25213  iscau4  25226  minveclem7  25382  elovolm  25423  dyaddisjlem  25543  ismbfd  25587  itg1mulc  25652  dvlip  25945  dvcvx  25972  plypf1  26164  eff1olem  26504  logccv  26619  lawcos  26773  leibpilem1  26897  sqff1o  27139  dvdsppwf1o  27143  dvdsflf1o  27144  fsumdvdsmul  27152  fsumdvdsmulOLD  27154  sgmmul  27159  fsumvma  27171  bposlem6  27247  lgsdchr  27313  rpvmasum2  27470  pntpbnd1  27544  ostthlem1  27585  sltres  27621  nodenselem5  27647  nodenselem6  27648  nodense  27651  addsproplem2  27933  mulsuniflem  28108  mulsunif2lem  28128  precsexlem9  28173  precsexlem10  28174  precsexlem11  28175  om2noseqlt2  28250  om2noseqf1o  28251  zs12ge0  28413  tgbtwntriv2  28485  ercgrg  28515  hlpasch  28754  colinearalglem4  28908  axlowdimlem15  28955  axcontlem7  28969  axcontlem8  28970  axcontlem10  28972  usgr1v  29255  pthdivtx  29726  clwwlkn1loopb  30044  grpolcan  30531  nvmf  30646  sspmval  30734  nmosetre  30765  minvecolem7  30884  hiassdi  31092  shscli  31318  fh1  31619  fh2  31620  cm2j  31621  chscllem2  31639  spansncvi  31653  5oalem2  31656  adjsym  31834  nmopsetretALT  31864  nmfnsetre  31878  cnvadj  31893  cnvunop  31919  unoplin  31921  hmoplin  31943  lnopmi  32001  hmops  32021  hmopm  32022  nmcexi  32027  adjlnop  32087  adjmul  32093  adjadd  32094  opsqrlem1  32141  mdsl0  32311  ssmd2  32313  mdexchi  32336  superpos  32355  chrelat2i  32366  atcvatlem  32386  atcvati  32387  chirredlem1  32391  chirredi  32395  atcvat3i  32397  atcvat4i  32398  mdsymlem3  32406  mdsymlem5  32408  cdj3lem2b  32438  ifnebib  32550  isoun  32707  xrge0infss  32768  1arithufdlem3  33555  extdg1id  33751  ddemeas  34321  fsum2dsub  34692  hgt750lemb  34741  bnj1145  35077  subfacp1lem3  35298  subfacp1lem5  35300  cvxpconn  35358  satfv1lem  35478  btwnconn1lem12  36214  colinbtwnle  36234  broutsideof2  36238  lineelsb2  36264  nn0prpwlem  36438  neibastop2lem  36476  tailfb  36493  onsuct0  36557  finxpreclem2  37507  lindsenlbs  37728  poimirlem4  37737  poimirlem26  37759  poimirlem27  37760  poimirlem31  37764  heicant  37768  mblfinlem2  37771  mblfinlem3  37772  ismblfin  37774  ftc1anclem5  37810  ftc1anclem6  37811  ftc1anc  37814  sdclem1  37856  seqpo  37860  sstotbnd  37888  cntotbnd  37909  ismtycnv  37915  ismtyres  37921  heibor  37934  exidreslem  37990  ghomdiv  38005  grpokerinj  38006  rngohomco  38087  rngoisoco  38095  idlsubcl  38136  divrngidl  38141  ispridl2  38151  ispridlc  38183  riotasv3d  39132  omllaw3  39417  omlfh1N  39430  hlrelat2  39575  cvratlem  39593  cvrat  39594  cvrat3  39614  cvrat4  39615  ps-2  39650  elpaddn0  39972  paddss12  39991  pmodlem2  40019  cdleme0cq  40387  cdlemeg49lebilem  40711  cdleme50eq  40713  tendoeq2  40946  tendoex  41147  diameetN  41228  diainN  41229  dvhopN  41288  djajN  41309  dihmeetcl  41517  mapdheq2  41901  3factsumint1  42187  imacrhmcl  42684  psrmnd  42713  evlselvlem  42744  fsuppind  42748  0prjspn  42786  fphpdo  42974  pell1234qrne0  43010  pell14qrgt0  43016  pell1qrge1  43027  monotoddzzfi  43099  jm2.18  43145  wepwsolem  43199  dnnumch3  43204  dnwech  43205  kelac1  43220  kercvrlsm  43240  onov0suclim  43431  cantnfresb  43481  dssmapnvod  44177  gsumws3  44353  gsumws4  44354  mnuprdlem1  44429  mnuprdlem2  44430  traxext  45134  modelac8prim  45149  cncmpmax  45193  fiiuncl  45226  choicefi  45360  mullimc  45778  mullimcf  45785  idlimc  45788  limclner  45811  climleltrp  45836  limsupub  45864  climuzlem  45903  climliminflimsup2  45969  xlimbr  45987  xlimxrre  45991  dfxlim2v  46007  fperdvper  46079  ioodvbdlimc1lem2  46092  ioodvbdlimc2lem  46094  dvnprodlem1  46106  stoweidlem27  46187  stoweidlem48  46208  fourierdlem42  46309  fourierdlem63  46329  fourierdlem65  46331  dfsalgen2  46501  subsaliuncl  46518  sge0iunmptlemfi  46573  sge0rpcpnf  46581  iundjiun  46620  psmeasure  46631  ovnsubaddlem2  46731  hoidmvle  46760  ovolval4lem2  46810  smflimlem2  46932  smflimlem3  46933  smflimlem6  46936  smflimmpt  46970  fcoresf1  47231  icceuelpart  47598  gpgedgvtx0  48223  gpgedgvtx1  48224  srhmsubcALTV  48487  catprs  49172  thincciso2  49616  functermclem  49668  functermc  49669  fulltermc  49672