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  5565  opabssxpd  5688  frpoind  6318  ordelord  6357  f1un  6823  fvelima2  6916  f1cofveqaeqALT  7236  isocnv  7308  isores2  7311  f1oiso2  7330  offval  7665  ordsucun  7803  xp2nd  8004  2ndconst  8083  sexp2  8128  smoord  8337  tfrlem9  8356  tfrlem11  8359  oaass  8528  omordi  8533  omwordri  8539  odi  8546  oewordri  8559  nnawordi  8588  nnmordi  8598  coflton  8638  dom2lem  8966  fundmen  9005  sbthlem9  9065  mapen  9111  mapunen  9116  ssenen  9121  domfi  9159  mapfien  9366  inf3lem6  9593  ttrclselem2  9686  frind  9710  r1val1  9746  rankval3b  9786  numacn  10009  infxpabs  10171  infxp  10174  cfsmolem  10230  infpssrlem4  10266  fin23lem27  10288  isf34lem4  10337  hsmexlem2  10387  axdc3lem2  10411  axdc3lem4  10413  iundom2g  10500  gchen1  10585  fpwwe2lem6  10596  fpwwe2lem10  10600  fpwwe2lem11  10601  prlem936  11007  muladd  11617  leord1  11712  eqord1  11713  ltord2  11714  leord2  11715  eqord2  11716  divadddiv  11904  ltmul12a  12045  lemul12b  12046  fimaxre  12134  supadd  12158  supmullem1  12160  cju  12189  zextlt  12615  zmax  12911  xrre  13136  supxr  13280  ixxdisj  13328  iooshf  13394  icodisj  13444  ioojoin  13451  iccshftr  13454  iccshftl  13456  iccdil  13458  icccntr  13460  iccf1o  13464  fzaddel  13526  fzsubel  13528  modadd1  13877  modmul1  13896  seqcaopr  14011  expsub  14082  expmordi  14139  sqlecan  14181  facndiv  14260  hashss  14381  hashfacen  14426  hashf1lem1  14427  fi1uzind  14479  brfi1indALT  14482  ccatpfx  14673  swrdccatfn  14696  swrdccatin2  14701  2cshwcshw  14798  resqrex  15223  fprodeq0  15948  lcmdvds  16585  hashdvds  16752  eulerthlem2  16759  pceu  16824  pcqcl  16834  infpnlem1  16888  4sqlem11  16933  ramcl  17007  prmgaplem5  17033  imasvscafn  17507  invfun  17733  initoeu2lem2  17984  catcisolem  18079  funcestrcsetclem8  18115  fullestrcsetc  18119  embedsetcestrclem  18125  funcsetcestrclem8  18130  fullsetcestrc  18134  prfcl  18171  prf1st  18172  prf2nd  18173  1st2ndprf  18174  curfuncf  18206  ipodrsfi  18505  mgmhmpropd  18632  subsubmgm  18644  mhmpropd  18726  subsubm  18750  pwsdiagmhm  18765  frmdgsum  18796  grplcan  18939  grplmulf1o  18952  grpraddf1o  18953  dfgrp3lem  18977  mulgsubcl  19027  subsubg  19088  eqger  19117  qus0subgadd  19138  resghm  19171  conjghm  19188  orbsta  19252  psgnunilem2  19432  odmulg  19493  sylow2a  19556  sylow3lem1  19564  lsmssv  19580  pj1ghm  19640  frgpup1  19712  ghmplusg  19783  subsubrng  20479  subsubrg  20514  srhmsubc  20596  issrngd  20771  lmhmco  20957  lmhmf1o  20960  lmhmima  20961  lmhmpreima  20962  reslmhm  20966  pwsdiaglmhm  20971  pwssplit2  20974  pwssplit3  20975  pj1lmhm  21014  lspdisj  21042  rngqiprngghmlem2  21205  rngqiprngghm  21216  prmirred  21391  cygznlem3  21486  frlmsslsp  21712  frlmlbs  21713  frlmup1  21714  issubassa2  21808  psrbagconf1o  21845  psrgrp  21872  evlslem2  21993  evlslem1  21996  ply1sclf1  22182  mamuass  22296  dmatmul  22391  dmatsubcl  22392  dmatmulcl  22394  dmatcrng  22396  scmatcrng  22415  mdetunilem9  22514  pm2mpghm  22710  fvmptnn04ifb  22745  toponmre  22987  neiptopreu  23027  ordtbas  23086  txcls  23498  txlm  23542  qtoptop2  23593  qtoprest  23611  kqt0lem  23630  ptuncnv  23701  fmfnfmlem4  23851  alexsubALTlem2  23942  tgpmulg  23987  blin  24316  xmeter  24328  xmetresbl  24332  dscmet  24467  nmdvr  24565  metnrmlem3  24757  icccvx  24855  bndth  24864  htpycc  24886  pcohtpylem  24926  pi1blem  24946  lmmbrf  25169  iscfil2  25173  iscau4  25186  minveclem7  25342  elovolm  25383  dyaddisjlem  25503  ismbfd  25547  itg1mulc  25612  dvlip  25905  dvcvx  25932  plypf1  26124  eff1olem  26464  logccv  26579  lawcos  26733  leibpilem1  26857  sqff1o  27099  dvdsppwf1o  27103  dvdsflf1o  27104  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  sgmmul  27119  fsumvma  27131  bposlem6  27207  lgsdchr  27273  rpvmasum2  27430  pntpbnd1  27504  ostthlem1  27545  sltres  27581  nodenselem5  27607  nodenselem6  27608  nodense  27611  addsproplem2  27884  mulsuniflem  28059  mulsunif2lem  28079  precsexlem9  28124  precsexlem10  28125  precsexlem11  28126  om2noseqlt2  28201  om2noseqf1o  28202  zs12ge0  28349  tgbtwntriv2  28421  ercgrg  28451  hlpasch  28690  colinearalglem4  28843  axlowdimlem15  28890  axcontlem7  28904  axcontlem8  28905  axcontlem10  28907  usgr1v  29190  pthdivtx  29664  clwwlkn1loopb  29979  grpolcan  30466  nvmf  30581  sspmval  30669  nmosetre  30700  minvecolem7  30819  hiassdi  31027  shscli  31253  fh1  31554  fh2  31555  cm2j  31556  chscllem2  31574  spansncvi  31588  5oalem2  31591  adjsym  31769  nmopsetretALT  31799  nmfnsetre  31813  cnvadj  31828  cnvunop  31854  unoplin  31856  hmoplin  31878  lnopmi  31936  hmops  31956  hmopm  31957  nmcexi  31962  adjlnop  32022  adjmul  32028  adjadd  32029  opsqrlem1  32076  mdsl0  32246  ssmd2  32248  mdexchi  32271  superpos  32290  chrelat2i  32301  atcvatlem  32321  atcvati  32322  chirredlem1  32326  chirredi  32330  atcvat3i  32332  atcvat4i  32333  mdsymlem3  32341  mdsymlem5  32343  cdj3lem2b  32373  ifnebib  32485  isoun  32632  xrge0infss  32690  1arithufdlem3  33524  extdg1id  33668  ddemeas  34233  fsum2dsub  34605  hgt750lemb  34654  bnj1145  34990  subfacp1lem3  35176  subfacp1lem5  35178  cvxpconn  35236  satfv1lem  35356  btwnconn1lem12  36093  colinbtwnle  36113  broutsideof2  36117  lineelsb2  36143  nn0prpwlem  36317  neibastop2lem  36355  tailfb  36372  onsuct0  36436  finxpreclem2  37385  lindsenlbs  37616  poimirlem4  37625  poimirlem26  37647  poimirlem27  37648  poimirlem31  37652  heicant  37656  mblfinlem2  37659  mblfinlem3  37660  ismblfin  37662  ftc1anclem5  37698  ftc1anclem6  37699  ftc1anc  37702  sdclem1  37744  seqpo  37748  sstotbnd  37776  cntotbnd  37797  ismtycnv  37803  ismtyres  37809  heibor  37822  exidreslem  37878  ghomdiv  37893  grpokerinj  37894  rngohomco  37975  rngoisoco  37983  idlsubcl  38024  divrngidl  38029  ispridl2  38039  ispridlc  38071  riotasv3d  38960  omllaw3  39245  omlfh1N  39258  hlrelat2  39404  cvratlem  39422  cvrat  39423  cvrat3  39443  cvrat4  39444  ps-2  39479  elpaddn0  39801  paddss12  39820  pmodlem2  39848  cdleme0cq  40216  cdlemeg49lebilem  40540  cdleme50eq  40542  tendoeq2  40775  tendoex  40976  diameetN  41057  diainN  41058  dvhopN  41117  djajN  41138  dihmeetcl  41346  mapdheq2  41730  3factsumint1  42016  imacrhmcl  42509  psrmnd  42540  evlsvvval  42558  evlselvlem  42581  fsuppind  42585  0prjspn  42623  fphpdo  42812  pell1234qrne0  42848  pell14qrgt0  42854  pell1qrge1  42865  monotoddzzfi  42938  jm2.18  42984  wepwsolem  43038  dnnumch3  43043  dnwech  43044  kelac1  43059  kercvrlsm  43079  onov0suclim  43270  cantnfresb  43320  dssmapnvod  44016  gsumws3  44192  gsumws4  44193  mnuprdlem1  44268  mnuprdlem2  44269  traxext  44974  modelac8prim  44989  cncmpmax  45033  fiiuncl  45066  choicefi  45201  mullimc  45621  mullimcf  45628  idlimc  45631  limclner  45656  climleltrp  45681  limsupub  45709  climuzlem  45748  climliminflimsup2  45814  xlimbr  45832  xlimxrre  45836  dfxlim2v  45852  fperdvper  45924  ioodvbdlimc1lem2  45937  ioodvbdlimc2lem  45939  dvnprodlem1  45951  stoweidlem27  46032  stoweidlem48  46053  fourierdlem42  46154  fourierdlem63  46174  fourierdlem65  46176  dfsalgen2  46346  subsaliuncl  46363  sge0iunmptlemfi  46418  sge0rpcpnf  46426  iundjiun  46465  psmeasure  46476  ovnsubaddlem2  46576  hoidmvle  46605  ovolval4lem2  46655  smflimlem2  46777  smflimlem3  46778  smflimlem6  46781  smflimmpt  46815  fcoresf1  47074  icceuelpart  47441  gpgedgvtx0  48056  gpgedgvtx1  48057  srhmsubcALTV  48317  catprs  49004  thincciso2  49448  functermclem  49500  functermc  49501  fulltermc  49504