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  5547  opabssxpd  5670  frpoind  6294  ordelord  6333  f1un  6788  fvelima2  6879  f1cofveqaeqALT  7199  isocnv  7271  isores2  7274  f1oiso2  7293  offval  7626  ordsucun  7764  xp2nd  7964  2ndconst  8041  sexp2  8086  smoord  8295  tfrlem9  8314  tfrlem11  8317  oaass  8486  omordi  8491  omwordri  8497  odi  8504  oewordri  8517  nnawordi  8546  nnmordi  8556  coflton  8596  dom2lem  8924  fundmen  8963  sbthlem9  9019  mapen  9065  mapunen  9070  ssenen  9075  domfi  9113  mapfien  9317  inf3lem6  9548  ttrclselem2  9641  frind  9665  r1val1  9701  rankval3b  9741  numacn  9962  infxpabs  10124  infxp  10127  cfsmolem  10183  infpssrlem4  10219  fin23lem27  10241  isf34lem4  10290  hsmexlem2  10340  axdc3lem2  10364  axdc3lem4  10366  iundom2g  10453  gchen1  10538  fpwwe2lem6  10549  fpwwe2lem10  10553  fpwwe2lem11  10554  prlem936  10960  muladd  11571  leord1  11666  eqord1  11667  ltord2  11668  leord2  11669  eqord2  11670  divadddiv  11858  ltmul12a  11999  lemul12b  12000  fimaxre  12088  supadd  12112  supmullem1  12114  cju  12143  zextlt  12569  zmax  12865  xrre  13090  supxr  13234  ixxdisj  13282  iooshf  13348  icodisj  13398  ioojoin  13405  iccshftr  13408  iccshftl  13410  iccdil  13412  icccntr  13414  iccf1o  13418  fzaddel  13480  fzsubel  13482  modadd1  13831  modmul1  13850  seqcaopr  13965  expsub  14036  expmordi  14093  sqlecan  14135  facndiv  14214  hashss  14335  hashfacen  14380  hashf1lem1  14381  fi1uzind  14433  brfi1indALT  14436  ccatpfx  14626  swrdccatfn  14649  swrdccatin2  14654  2cshwcshw  14751  resqrex  15176  fprodeq0  15901  lcmdvds  16538  hashdvds  16705  eulerthlem2  16712  pceu  16777  pcqcl  16787  infpnlem1  16841  4sqlem11  16886  ramcl  16960  prmgaplem5  16986  imasvscafn  17460  invfun  17690  initoeu2lem2  17941  catcisolem  18036  funcestrcsetclem8  18072  fullestrcsetc  18076  embedsetcestrclem  18082  funcsetcestrclem8  18087  fullsetcestrc  18091  prfcl  18128  prf1st  18129  prf2nd  18130  1st2ndprf  18131  curfuncf  18163  ipodrsfi  18464  mgmhmpropd  18591  subsubmgm  18603  mhmpropd  18685  subsubm  18709  pwsdiagmhm  18724  frmdgsum  18755  grplcan  18898  grplmulf1o  18911  grpraddf1o  18912  dfgrp3lem  18936  mulgsubcl  18986  subsubg  19047  eqger  19076  qus0subgadd  19097  resghm  19130  conjghm  19147  orbsta  19211  psgnunilem2  19393  odmulg  19454  sylow2a  19517  sylow3lem1  19525  lsmssv  19541  pj1ghm  19601  frgpup1  19673  ghmplusg  19744  subsubrng  20467  subsubrg  20502  srhmsubc  20584  issrngd  20759  lmhmco  20966  lmhmf1o  20969  lmhmima  20970  lmhmpreima  20971  reslmhm  20975  pwsdiaglmhm  20980  pwssplit2  20983  pwssplit3  20984  pj1lmhm  21023  lspdisj  21051  rngqiprngghmlem2  21214  rngqiprngghm  21225  prmirred  21400  cygznlem3  21495  frlmsslsp  21722  frlmlbs  21723  frlmup1  21724  issubassa2  21818  psrbagconf1o  21855  psrgrp  21882  evlslem2  22003  evlslem1  22006  ply1sclf1  22192  mamuass  22306  dmatmul  22401  dmatsubcl  22402  dmatmulcl  22404  dmatcrng  22406  scmatcrng  22425  mdetunilem9  22524  pm2mpghm  22720  fvmptnn04ifb  22755  toponmre  22997  neiptopreu  23037  ordtbas  23096  txcls  23508  txlm  23552  qtoptop2  23603  qtoprest  23621  kqt0lem  23640  ptuncnv  23711  fmfnfmlem4  23861  alexsubALTlem2  23952  tgpmulg  23997  blin  24326  xmeter  24338  xmetresbl  24342  dscmet  24477  nmdvr  24575  metnrmlem3  24767  icccvx  24865  bndth  24874  htpycc  24896  pcohtpylem  24936  pi1blem  24956  lmmbrf  25179  iscfil2  25183  iscau4  25196  minveclem7  25352  elovolm  25393  dyaddisjlem  25513  ismbfd  25557  itg1mulc  25622  dvlip  25915  dvcvx  25942  plypf1  26134  eff1olem  26474  logccv  26589  lawcos  26743  leibpilem1  26867  sqff1o  27109  dvdsppwf1o  27113  dvdsflf1o  27114  fsumdvdsmul  27122  fsumdvdsmulOLD  27124  sgmmul  27129  fsumvma  27141  bposlem6  27217  lgsdchr  27283  rpvmasum2  27440  pntpbnd1  27514  ostthlem1  27555  sltres  27591  nodenselem5  27617  nodenselem6  27618  nodense  27621  addsproplem2  27901  mulsuniflem  28076  mulsunif2lem  28096  precsexlem9  28141  precsexlem10  28142  precsexlem11  28143  om2noseqlt2  28218  om2noseqf1o  28219  zs12ge0  28379  tgbtwntriv2  28451  ercgrg  28481  hlpasch  28720  colinearalglem4  28873  axlowdimlem15  28920  axcontlem7  28934  axcontlem8  28935  axcontlem10  28937  usgr1v  29220  pthdivtx  29691  clwwlkn1loopb  30006  grpolcan  30493  nvmf  30608  sspmval  30696  nmosetre  30727  minvecolem7  30846  hiassdi  31054  shscli  31280  fh1  31581  fh2  31582  cm2j  31583  chscllem2  31601  spansncvi  31615  5oalem2  31618  adjsym  31796  nmopsetretALT  31826  nmfnsetre  31840  cnvadj  31855  cnvunop  31881  unoplin  31883  hmoplin  31905  lnopmi  31963  hmops  31983  hmopm  31984  nmcexi  31989  adjlnop  32049  adjmul  32055  adjadd  32056  opsqrlem1  32103  mdsl0  32273  ssmd2  32275  mdexchi  32298  superpos  32317  chrelat2i  32328  atcvatlem  32348  atcvati  32349  chirredlem1  32353  chirredi  32357  atcvat3i  32359  atcvat4i  32360  mdsymlem3  32368  mdsymlem5  32370  cdj3lem2b  32400  ifnebib  32512  isoun  32663  xrge0infss  32722  1arithufdlem3  33502  extdg1id  33652  ddemeas  34222  fsum2dsub  34594  hgt750lemb  34643  bnj1145  34979  subfacp1lem3  35174  subfacp1lem5  35176  cvxpconn  35234  satfv1lem  35354  btwnconn1lem12  36091  colinbtwnle  36111  broutsideof2  36115  lineelsb2  36141  nn0prpwlem  36315  neibastop2lem  36353  tailfb  36370  onsuct0  36434  finxpreclem2  37383  lindsenlbs  37614  poimirlem4  37623  poimirlem26  37645  poimirlem27  37646  poimirlem31  37650  heicant  37654  mblfinlem2  37657  mblfinlem3  37658  ismblfin  37660  ftc1anclem5  37696  ftc1anclem6  37697  ftc1anc  37700  sdclem1  37742  seqpo  37746  sstotbnd  37774  cntotbnd  37795  ismtycnv  37801  ismtyres  37807  heibor  37820  exidreslem  37876  ghomdiv  37891  grpokerinj  37892  rngohomco  37973  rngoisoco  37981  idlsubcl  38022  divrngidl  38027  ispridl2  38037  ispridlc  38069  riotasv3d  38958  omllaw3  39243  omlfh1N  39256  hlrelat2  39402  cvratlem  39420  cvrat  39421  cvrat3  39441  cvrat4  39442  ps-2  39477  elpaddn0  39799  paddss12  39818  pmodlem2  39846  cdleme0cq  40214  cdlemeg49lebilem  40538  cdleme50eq  40540  tendoeq2  40773  tendoex  40974  diameetN  41055  diainN  41056  dvhopN  41115  djajN  41136  dihmeetcl  41344  mapdheq2  41728  3factsumint1  42014  imacrhmcl  42507  psrmnd  42538  evlsvvval  42556  evlselvlem  42579  fsuppind  42583  0prjspn  42621  fphpdo  42810  pell1234qrne0  42846  pell14qrgt0  42852  pell1qrge1  42863  monotoddzzfi  42935  jm2.18  42981  wepwsolem  43035  dnnumch3  43040  dnwech  43041  kelac1  43056  kercvrlsm  43076  onov0suclim  43267  cantnfresb  43317  dssmapnvod  44013  gsumws3  44189  gsumws4  44190  mnuprdlem1  44265  mnuprdlem2  44266  traxext  44971  modelac8prim  44986  cncmpmax  45030  fiiuncl  45063  choicefi  45198  mullimc  45617  mullimcf  45624  idlimc  45627  limclner  45652  climleltrp  45677  limsupub  45705  climuzlem  45744  climliminflimsup2  45810  xlimbr  45828  xlimxrre  45832  dfxlim2v  45848  fperdvper  45920  ioodvbdlimc1lem2  45933  ioodvbdlimc2lem  45935  dvnprodlem1  45947  stoweidlem27  46028  stoweidlem48  46049  fourierdlem42  46150  fourierdlem63  46170  fourierdlem65  46172  dfsalgen2  46342  subsaliuncl  46359  sge0iunmptlemfi  46414  sge0rpcpnf  46422  iundjiun  46461  psmeasure  46472  ovnsubaddlem2  46572  hoidmvle  46601  ovolval4lem2  46651  smflimlem2  46773  smflimlem3  46774  smflimlem6  46777  smflimmpt  46811  fcoresf1  47073  icceuelpart  47440  gpgedgvtx0  48065  gpgedgvtx1  48066  srhmsubcALTV  48329  catprs  49016  thincciso2  49460  functermclem  49512  functermc  49513  fulltermc  49516