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  5555  opabssxpd  5678  frpoind  6303  ordelord  6342  f1un  6802  fvelima2  6895  f1cofveqaeqALT  7215  isocnv  7287  isores2  7290  f1oiso2  7309  offval  7642  ordsucun  7780  xp2nd  7980  2ndconst  8057  sexp2  8102  smoord  8311  tfrlem9  8330  tfrlem11  8333  oaass  8502  omordi  8507  omwordri  8513  odi  8520  oewordri  8533  nnawordi  8562  nnmordi  8572  coflton  8612  dom2lem  8940  fundmen  8979  sbthlem9  9036  mapen  9082  mapunen  9087  ssenen  9092  domfi  9130  mapfien  9335  inf3lem6  9562  ttrclselem2  9655  frind  9679  r1val1  9715  rankval3b  9755  numacn  9978  infxpabs  10140  infxp  10143  cfsmolem  10199  infpssrlem4  10235  fin23lem27  10257  isf34lem4  10306  hsmexlem2  10356  axdc3lem2  10380  axdc3lem4  10382  iundom2g  10469  gchen1  10554  fpwwe2lem6  10565  fpwwe2lem10  10569  fpwwe2lem11  10570  prlem936  10976  muladd  11586  leord1  11681  eqord1  11682  ltord2  11683  leord2  11684  eqord2  11685  divadddiv  11873  ltmul12a  12014  lemul12b  12015  fimaxre  12103  supadd  12127  supmullem1  12129  cju  12158  zextlt  12584  zmax  12880  xrre  13105  supxr  13249  ixxdisj  13297  iooshf  13363  icodisj  13413  ioojoin  13420  iccshftr  13423  iccshftl  13425  iccdil  13427  icccntr  13429  iccf1o  13433  fzaddel  13495  fzsubel  13497  modadd1  13846  modmul1  13865  seqcaopr  13980  expsub  14051  expmordi  14108  sqlecan  14150  facndiv  14229  hashss  14350  hashfacen  14395  hashf1lem1  14396  fi1uzind  14448  brfi1indALT  14451  ccatpfx  14642  swrdccatfn  14665  swrdccatin2  14670  2cshwcshw  14767  resqrex  15192  fprodeq0  15917  lcmdvds  16554  hashdvds  16721  eulerthlem2  16728  pceu  16793  pcqcl  16803  infpnlem1  16857  4sqlem11  16902  ramcl  16976  prmgaplem5  17002  imasvscafn  17476  invfun  17702  initoeu2lem2  17953  catcisolem  18048  funcestrcsetclem8  18084  fullestrcsetc  18088  embedsetcestrclem  18094  funcsetcestrclem8  18099  fullsetcestrc  18103  prfcl  18140  prf1st  18141  prf2nd  18142  1st2ndprf  18143  curfuncf  18175  ipodrsfi  18474  mgmhmpropd  18601  subsubmgm  18613  mhmpropd  18695  subsubm  18719  pwsdiagmhm  18734  frmdgsum  18765  grplcan  18908  grplmulf1o  18921  grpraddf1o  18922  dfgrp3lem  18946  mulgsubcl  18996  subsubg  19057  eqger  19086  qus0subgadd  19107  resghm  19140  conjghm  19157  orbsta  19221  psgnunilem2  19401  odmulg  19462  sylow2a  19525  sylow3lem1  19533  lsmssv  19549  pj1ghm  19609  frgpup1  19681  ghmplusg  19752  subsubrng  20448  subsubrg  20483  srhmsubc  20565  issrngd  20740  lmhmco  20926  lmhmf1o  20929  lmhmima  20930  lmhmpreima  20931  reslmhm  20935  pwsdiaglmhm  20940  pwssplit2  20943  pwssplit3  20944  pj1lmhm  20983  lspdisj  21011  rngqiprngghmlem2  21174  rngqiprngghm  21185  prmirred  21360  cygznlem3  21455  frlmsslsp  21681  frlmlbs  21682  frlmup1  21683  issubassa2  21777  psrbagconf1o  21814  psrgrp  21841  evlslem2  21962  evlslem1  21965  ply1sclf1  22151  mamuass  22265  dmatmul  22360  dmatsubcl  22361  dmatmulcl  22363  dmatcrng  22365  scmatcrng  22384  mdetunilem9  22483  pm2mpghm  22679  fvmptnn04ifb  22714  toponmre  22956  neiptopreu  22996  ordtbas  23055  txcls  23467  txlm  23511  qtoptop2  23562  qtoprest  23580  kqt0lem  23599  ptuncnv  23670  fmfnfmlem4  23820  alexsubALTlem2  23911  tgpmulg  23956  blin  24285  xmeter  24297  xmetresbl  24301  dscmet  24436  nmdvr  24534  metnrmlem3  24726  icccvx  24824  bndth  24833  htpycc  24855  pcohtpylem  24895  pi1blem  24915  lmmbrf  25138  iscfil2  25142  iscau4  25155  minveclem7  25311  elovolm  25352  dyaddisjlem  25472  ismbfd  25516  itg1mulc  25581  dvlip  25874  dvcvx  25901  plypf1  26093  eff1olem  26433  logccv  26548  lawcos  26702  leibpilem1  26826  sqff1o  27068  dvdsppwf1o  27072  dvdsflf1o  27073  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  sgmmul  27088  fsumvma  27100  bposlem6  27176  lgsdchr  27242  rpvmasum2  27399  pntpbnd1  27473  ostthlem1  27514  sltres  27550  nodenselem5  27576  nodenselem6  27577  nodense  27580  addsproplem2  27853  mulsuniflem  28028  mulsunif2lem  28048  precsexlem9  28093  precsexlem10  28094  precsexlem11  28095  om2noseqlt2  28170  om2noseqf1o  28171  zs12ge0  28318  tgbtwntriv2  28390  ercgrg  28420  hlpasch  28659  colinearalglem4  28812  axlowdimlem15  28859  axcontlem7  28873  axcontlem8  28874  axcontlem10  28876  usgr1v  29159  pthdivtx  29630  clwwlkn1loopb  29945  grpolcan  30432  nvmf  30547  sspmval  30635  nmosetre  30666  minvecolem7  30785  hiassdi  30993  shscli  31219  fh1  31520  fh2  31521  cm2j  31522  chscllem2  31540  spansncvi  31554  5oalem2  31557  adjsym  31735  nmopsetretALT  31765  nmfnsetre  31779  cnvadj  31794  cnvunop  31820  unoplin  31822  hmoplin  31844  lnopmi  31902  hmops  31922  hmopm  31923  nmcexi  31928  adjlnop  31988  adjmul  31994  adjadd  31995  opsqrlem1  32042  mdsl0  32212  ssmd2  32214  mdexchi  32237  superpos  32256  chrelat2i  32267  atcvatlem  32287  atcvati  32288  chirredlem1  32292  chirredi  32296  atcvat3i  32298  atcvat4i  32299  mdsymlem3  32307  mdsymlem5  32309  cdj3lem2b  32339  ifnebib  32451  isoun  32598  xrge0infss  32656  1arithufdlem3  33490  extdg1id  33634  ddemeas  34199  fsum2dsub  34571  hgt750lemb  34620  bnj1145  34956  subfacp1lem3  35142  subfacp1lem5  35144  cvxpconn  35202  satfv1lem  35322  btwnconn1lem12  36059  colinbtwnle  36079  broutsideof2  36083  lineelsb2  36109  nn0prpwlem  36283  neibastop2lem  36321  tailfb  36338  onsuct0  36402  finxpreclem2  37351  lindsenlbs  37582  poimirlem4  37591  poimirlem26  37613  poimirlem27  37614  poimirlem31  37618  heicant  37622  mblfinlem2  37625  mblfinlem3  37626  ismblfin  37628  ftc1anclem5  37664  ftc1anclem6  37665  ftc1anc  37668  sdclem1  37710  seqpo  37714  sstotbnd  37742  cntotbnd  37763  ismtycnv  37769  ismtyres  37775  heibor  37788  exidreslem  37844  ghomdiv  37859  grpokerinj  37860  rngohomco  37941  rngoisoco  37949  idlsubcl  37990  divrngidl  37995  ispridl2  38005  ispridlc  38037  riotasv3d  38926  omllaw3  39211  omlfh1N  39224  hlrelat2  39370  cvratlem  39388  cvrat  39389  cvrat3  39409  cvrat4  39410  ps-2  39445  elpaddn0  39767  paddss12  39786  pmodlem2  39814  cdleme0cq  40182  cdlemeg49lebilem  40506  cdleme50eq  40508  tendoeq2  40741  tendoex  40942  diameetN  41023  diainN  41024  dvhopN  41083  djajN  41104  dihmeetcl  41312  mapdheq2  41696  3factsumint1  41982  imacrhmcl  42475  psrmnd  42506  evlsvvval  42524  evlselvlem  42547  fsuppind  42551  0prjspn  42589  fphpdo  42778  pell1234qrne0  42814  pell14qrgt0  42820  pell1qrge1  42831  monotoddzzfi  42904  jm2.18  42950  wepwsolem  43004  dnnumch3  43009  dnwech  43010  kelac1  43025  kercvrlsm  43045  onov0suclim  43236  cantnfresb  43286  dssmapnvod  43982  gsumws3  44158  gsumws4  44159  mnuprdlem1  44234  mnuprdlem2  44235  traxext  44940  modelac8prim  44955  cncmpmax  44999  fiiuncl  45032  choicefi  45167  mullimc  45587  mullimcf  45594  idlimc  45597  limclner  45622  climleltrp  45647  limsupub  45675  climuzlem  45714  climliminflimsup2  45780  xlimbr  45798  xlimxrre  45802  dfxlim2v  45818  fperdvper  45890  ioodvbdlimc1lem2  45903  ioodvbdlimc2lem  45905  dvnprodlem1  45917  stoweidlem27  45998  stoweidlem48  46019  fourierdlem42  46120  fourierdlem63  46140  fourierdlem65  46142  dfsalgen2  46312  subsaliuncl  46329  sge0iunmptlemfi  46384  sge0rpcpnf  46392  iundjiun  46431  psmeasure  46442  ovnsubaddlem2  46542  hoidmvle  46571  ovolval4lem2  46621  smflimlem2  46743  smflimlem3  46744  smflimlem6  46747  smflimmpt  46781  fcoresf1  47043  icceuelpart  47410  gpgedgvtx0  48025  gpgedgvtx1  48026  srhmsubcALTV  48286  catprs  48973  thincciso2  49417  functermclem  49469  functermc  49470  fulltermc  49473