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  5562  opabssxpd  5685  frpoind  6315  ordelord  6354  f1un  6820  fvelima2  6913  f1cofveqaeqALT  7233  isocnv  7305  isores2  7308  f1oiso2  7327  offval  7662  ordsucun  7800  xp2nd  8001  2ndconst  8080  sexp2  8125  smoord  8334  tfrlem9  8353  tfrlem11  8356  oaass  8525  omordi  8530  omwordri  8536  odi  8543  oewordri  8556  nnawordi  8585  nnmordi  8595  coflton  8635  dom2lem  8963  fundmen  9002  sbthlem9  9059  mapen  9105  mapunen  9110  ssenen  9115  domfi  9153  mapfien  9359  inf3lem6  9586  ttrclselem2  9679  frind  9703  r1val1  9739  rankval3b  9779  numacn  10002  infxpabs  10164  infxp  10167  cfsmolem  10223  infpssrlem4  10259  fin23lem27  10281  isf34lem4  10330  hsmexlem2  10380  axdc3lem2  10404  axdc3lem4  10406  iundom2g  10493  gchen1  10578  fpwwe2lem6  10589  fpwwe2lem10  10593  fpwwe2lem11  10594  prlem936  11000  muladd  11610  leord1  11705  eqord1  11706  ltord2  11707  leord2  11708  eqord2  11709  divadddiv  11897  ltmul12a  12038  lemul12b  12039  fimaxre  12127  supadd  12151  supmullem1  12153  cju  12182  zextlt  12608  zmax  12904  xrre  13129  supxr  13273  ixxdisj  13321  iooshf  13387  icodisj  13437  ioojoin  13444  iccshftr  13447  iccshftl  13449  iccdil  13451  icccntr  13453  iccf1o  13457  fzaddel  13519  fzsubel  13521  modadd1  13870  modmul1  13889  seqcaopr  14004  expsub  14075  expmordi  14132  sqlecan  14174  facndiv  14253  hashss  14374  hashfacen  14419  hashf1lem1  14420  fi1uzind  14472  brfi1indALT  14475  ccatpfx  14666  swrdccatfn  14689  swrdccatin2  14694  2cshwcshw  14791  resqrex  15216  fprodeq0  15941  lcmdvds  16578  hashdvds  16745  eulerthlem2  16752  pceu  16817  pcqcl  16827  infpnlem1  16881  4sqlem11  16926  ramcl  17000  prmgaplem5  17026  imasvscafn  17500  invfun  17726  initoeu2lem2  17977  catcisolem  18072  funcestrcsetclem8  18108  fullestrcsetc  18112  embedsetcestrclem  18118  funcsetcestrclem8  18123  fullsetcestrc  18127  prfcl  18164  prf1st  18165  prf2nd  18166  1st2ndprf  18167  curfuncf  18199  ipodrsfi  18498  mgmhmpropd  18625  subsubmgm  18637  mhmpropd  18719  subsubm  18743  pwsdiagmhm  18758  frmdgsum  18789  grplcan  18932  grplmulf1o  18945  grpraddf1o  18946  dfgrp3lem  18970  mulgsubcl  19020  subsubg  19081  eqger  19110  qus0subgadd  19131  resghm  19164  conjghm  19181  orbsta  19245  psgnunilem2  19425  odmulg  19486  sylow2a  19549  sylow3lem1  19557  lsmssv  19573  pj1ghm  19633  frgpup1  19705  ghmplusg  19776  subsubrng  20472  subsubrg  20507  srhmsubc  20589  issrngd  20764  lmhmco  20950  lmhmf1o  20953  lmhmima  20954  lmhmpreima  20955  reslmhm  20959  pwsdiaglmhm  20964  pwssplit2  20967  pwssplit3  20968  pj1lmhm  21007  lspdisj  21035  rngqiprngghmlem2  21198  rngqiprngghm  21209  prmirred  21384  cygznlem3  21479  frlmsslsp  21705  frlmlbs  21706  frlmup1  21707  issubassa2  21801  psrbagconf1o  21838  psrgrp  21865  evlslem2  21986  evlslem1  21989  ply1sclf1  22175  mamuass  22289  dmatmul  22384  dmatsubcl  22385  dmatmulcl  22387  dmatcrng  22389  scmatcrng  22408  mdetunilem9  22507  pm2mpghm  22703  fvmptnn04ifb  22738  toponmre  22980  neiptopreu  23020  ordtbas  23079  txcls  23491  txlm  23535  qtoptop2  23586  qtoprest  23604  kqt0lem  23623  ptuncnv  23694  fmfnfmlem4  23844  alexsubALTlem2  23935  tgpmulg  23980  blin  24309  xmeter  24321  xmetresbl  24325  dscmet  24460  nmdvr  24558  metnrmlem3  24750  icccvx  24848  bndth  24857  htpycc  24879  pcohtpylem  24919  pi1blem  24939  lmmbrf  25162  iscfil2  25166  iscau4  25179  minveclem7  25335  elovolm  25376  dyaddisjlem  25496  ismbfd  25540  itg1mulc  25605  dvlip  25898  dvcvx  25925  plypf1  26117  eff1olem  26457  logccv  26572  lawcos  26726  leibpilem1  26850  sqff1o  27092  dvdsppwf1o  27096  dvdsflf1o  27097  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  sgmmul  27112  fsumvma  27124  bposlem6  27200  lgsdchr  27266  rpvmasum2  27423  pntpbnd1  27497  ostthlem1  27538  sltres  27574  nodenselem5  27600  nodenselem6  27601  nodense  27604  addsproplem2  27877  mulsuniflem  28052  mulsunif2lem  28072  precsexlem9  28117  precsexlem10  28118  precsexlem11  28119  om2noseqlt2  28194  om2noseqf1o  28195  zs12ge0  28342  tgbtwntriv2  28414  ercgrg  28444  hlpasch  28683  colinearalglem4  28836  axlowdimlem15  28883  axcontlem7  28897  axcontlem8  28898  axcontlem10  28900  usgr1v  29183  pthdivtx  29657  clwwlkn1loopb  29972  grpolcan  30459  nvmf  30574  sspmval  30662  nmosetre  30693  minvecolem7  30812  hiassdi  31020  shscli  31246  fh1  31547  fh2  31548  cm2j  31549  chscllem2  31567  spansncvi  31581  5oalem2  31584  adjsym  31762  nmopsetretALT  31792  nmfnsetre  31806  cnvadj  31821  cnvunop  31847  unoplin  31849  hmoplin  31871  lnopmi  31929  hmops  31949  hmopm  31950  nmcexi  31955  adjlnop  32015  adjmul  32021  adjadd  32022  opsqrlem1  32069  mdsl0  32239  ssmd2  32241  mdexchi  32264  superpos  32283  chrelat2i  32294  atcvatlem  32314  atcvati  32315  chirredlem1  32319  chirredi  32323  atcvat3i  32325  atcvat4i  32326  mdsymlem3  32334  mdsymlem5  32336  cdj3lem2b  32366  ifnebib  32478  isoun  32625  xrge0infss  32683  1arithufdlem3  33517  extdg1id  33661  ddemeas  34226  fsum2dsub  34598  hgt750lemb  34647  bnj1145  34983  subfacp1lem3  35169  subfacp1lem5  35171  cvxpconn  35229  satfv1lem  35349  btwnconn1lem12  36086  colinbtwnle  36106  broutsideof2  36110  lineelsb2  36136  nn0prpwlem  36310  neibastop2lem  36348  tailfb  36365  onsuct0  36429  finxpreclem2  37378  lindsenlbs  37609  poimirlem4  37618  poimirlem26  37640  poimirlem27  37641  poimirlem31  37645  heicant  37649  mblfinlem2  37652  mblfinlem3  37653  ismblfin  37655  ftc1anclem5  37691  ftc1anclem6  37692  ftc1anc  37695  sdclem1  37737  seqpo  37741  sstotbnd  37769  cntotbnd  37790  ismtycnv  37796  ismtyres  37802  heibor  37815  exidreslem  37871  ghomdiv  37886  grpokerinj  37887  rngohomco  37968  rngoisoco  37976  idlsubcl  38017  divrngidl  38022  ispridl2  38032  ispridlc  38064  riotasv3d  38953  omllaw3  39238  omlfh1N  39251  hlrelat2  39397  cvratlem  39415  cvrat  39416  cvrat3  39436  cvrat4  39437  ps-2  39472  elpaddn0  39794  paddss12  39813  pmodlem2  39841  cdleme0cq  40209  cdlemeg49lebilem  40533  cdleme50eq  40535  tendoeq2  40768  tendoex  40969  diameetN  41050  diainN  41051  dvhopN  41110  djajN  41131  dihmeetcl  41339  mapdheq2  41723  3factsumint1  42009  imacrhmcl  42502  psrmnd  42533  evlsvvval  42551  evlselvlem  42574  fsuppind  42578  0prjspn  42616  fphpdo  42805  pell1234qrne0  42841  pell14qrgt0  42847  pell1qrge1  42858  monotoddzzfi  42931  jm2.18  42977  wepwsolem  43031  dnnumch3  43036  dnwech  43037  kelac1  43052  kercvrlsm  43072  onov0suclim  43263  cantnfresb  43313  dssmapnvod  44009  gsumws3  44185  gsumws4  44186  mnuprdlem1  44261  mnuprdlem2  44262  traxext  44967  modelac8prim  44982  cncmpmax  45026  fiiuncl  45059  choicefi  45194  mullimc  45614  mullimcf  45621  idlimc  45624  limclner  45649  climleltrp  45674  limsupub  45702  climuzlem  45741  climliminflimsup2  45807  xlimbr  45825  xlimxrre  45829  dfxlim2v  45845  fperdvper  45917  ioodvbdlimc1lem2  45930  ioodvbdlimc2lem  45932  dvnprodlem1  45944  stoweidlem27  46025  stoweidlem48  46046  fourierdlem42  46147  fourierdlem63  46167  fourierdlem65  46169  dfsalgen2  46339  subsaliuncl  46356  sge0iunmptlemfi  46411  sge0rpcpnf  46419  iundjiun  46458  psmeasure  46469  ovnsubaddlem2  46569  hoidmvle  46598  ovolval4lem2  46648  smflimlem2  46770  smflimlem3  46771  smflimlem6  46774  smflimmpt  46808  fcoresf1  47070  icceuelpart  47437  gpgedgvtx0  48052  gpgedgvtx1  48053  srhmsubcALTV  48313  catprs  49000  thincciso2  49444  functermclem  49496  functermc  49497  fulltermc  49500