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  5535  opabssxpd  5658  frpoind  6284  ordelord  6323  f1un  6778  fvelima2  6869  f1cofveqaeqALT  7187  isocnv  7259  isores2  7262  f1oiso2  7281  offval  7614  ordsucun  7750  xp2nd  7949  2ndconst  8026  sexp2  8071  smoord  8280  tfrlem9  8299  tfrlem11  8302  oaass  8471  omordi  8476  omwordri  8482  odi  8489  oewordri  8502  nnawordi  8531  nnmordi  8541  coflton  8581  dom2lem  8909  fundmen  8948  sbthlem9  9003  mapen  9049  mapunen  9054  ssenen  9059  domfi  9093  mapfien  9287  inf3lem6  9518  ttrclselem2  9611  frind  9638  r1val1  9674  rankval3b  9714  numacn  9935  infxpabs  10097  infxp  10100  cfsmolem  10156  infpssrlem4  10192  fin23lem27  10214  isf34lem4  10263  hsmexlem2  10313  axdc3lem2  10337  axdc3lem4  10339  iundom2g  10426  gchen1  10511  fpwwe2lem6  10522  fpwwe2lem10  10526  fpwwe2lem11  10527  prlem936  10933  muladd  11544  leord1  11639  eqord1  11640  ltord2  11641  leord2  11642  eqord2  11643  divadddiv  11831  ltmul12a  11972  lemul12b  11973  fimaxre  12061  supadd  12085  supmullem1  12087  cju  12116  zextlt  12542  zmax  12838  xrre  13063  supxr  13207  ixxdisj  13255  iooshf  13321  icodisj  13371  ioojoin  13378  iccshftr  13381  iccshftl  13383  iccdil  13385  icccntr  13387  iccf1o  13391  fzaddel  13453  fzsubel  13455  modadd1  13807  modmul1  13826  seqcaopr  13941  expsub  14012  expmordi  14069  sqlecan  14111  facndiv  14190  hashss  14311  hashfacen  14356  hashf1lem1  14357  fi1uzind  14409  brfi1indALT  14412  ccatpfx  14603  swrdccatfn  14626  swrdccatin2  14631  2cshwcshw  14727  resqrex  15152  fprodeq0  15877  lcmdvds  16514  hashdvds  16681  eulerthlem2  16688  pceu  16753  pcqcl  16763  infpnlem1  16817  4sqlem11  16862  ramcl  16936  prmgaplem5  16962  imasvscafn  17436  invfun  17666  initoeu2lem2  17917  catcisolem  18012  funcestrcsetclem8  18048  fullestrcsetc  18052  embedsetcestrclem  18058  funcsetcestrclem8  18063  fullsetcestrc  18067  prfcl  18104  prf1st  18105  prf2nd  18106  1st2ndprf  18107  curfuncf  18139  ipodrsfi  18440  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  19085  qus0subgadd  19106  resghm  19139  conjghm  19156  orbsta  19220  psgnunilem2  19402  odmulg  19463  sylow2a  19526  sylow3lem1  19534  lsmssv  19550  pj1ghm  19610  frgpup1  19682  ghmplusg  19753  subsubrng  20473  subsubrg  20508  srhmsubc  20590  issrngd  20765  lmhmco  20972  lmhmf1o  20975  lmhmima  20976  lmhmpreima  20977  reslmhm  20981  pwsdiaglmhm  20986  pwssplit2  20989  pwssplit3  20990  pj1lmhm  21029  lspdisj  21057  rngqiprngghmlem2  21220  rngqiprngghm  21231  prmirred  21406  cygznlem3  21501  frlmsslsp  21728  frlmlbs  21729  frlmup1  21730  issubassa2  21824  psrbagconf1o  21861  psrgrp  21888  evlslem2  22009  evlslem1  22012  ply1sclf1  22198  mamuass  22312  dmatmul  22407  dmatsubcl  22408  dmatmulcl  22410  dmatcrng  22412  scmatcrng  22431  mdetunilem9  22530  pm2mpghm  22726  fvmptnn04ifb  22761  toponmre  23003  neiptopreu  23043  ordtbas  23102  txcls  23514  txlm  23558  qtoptop2  23609  qtoprest  23627  kqt0lem  23646  ptuncnv  23717  fmfnfmlem4  23867  alexsubALTlem2  23958  tgpmulg  24003  blin  24331  xmeter  24343  xmetresbl  24347  dscmet  24482  nmdvr  24580  metnrmlem3  24772  icccvx  24870  bndth  24879  htpycc  24901  pcohtpylem  24941  pi1blem  24961  lmmbrf  25184  iscfil2  25188  iscau4  25201  minveclem7  25357  elovolm  25398  dyaddisjlem  25518  ismbfd  25562  itg1mulc  25627  dvlip  25920  dvcvx  25947  plypf1  26139  eff1olem  26479  logccv  26594  lawcos  26748  leibpilem1  26872  sqff1o  27114  dvdsppwf1o  27118  dvdsflf1o  27119  fsumdvdsmul  27127  fsumdvdsmulOLD  27129  sgmmul  27134  fsumvma  27146  bposlem6  27222  lgsdchr  27288  rpvmasum2  27445  pntpbnd1  27519  ostthlem1  27560  sltres  27596  nodenselem5  27622  nodenselem6  27623  nodense  27626  addsproplem2  27908  mulsuniflem  28083  mulsunif2lem  28103  precsexlem9  28148  precsexlem10  28149  precsexlem11  28150  om2noseqlt2  28225  om2noseqf1o  28226  zs12ge0  28388  tgbtwntriv2  28460  ercgrg  28490  hlpasch  28729  colinearalglem4  28882  axlowdimlem15  28929  axcontlem7  28943  axcontlem8  28944  axcontlem10  28946  usgr1v  29229  pthdivtx  29700  clwwlkn1loopb  30015  grpolcan  30502  nvmf  30617  sspmval  30705  nmosetre  30736  minvecolem7  30855  hiassdi  31063  shscli  31289  fh1  31590  fh2  31591  cm2j  31592  chscllem2  31610  spansncvi  31624  5oalem2  31627  adjsym  31805  nmopsetretALT  31835  nmfnsetre  31849  cnvadj  31864  cnvunop  31890  unoplin  31892  hmoplin  31914  lnopmi  31972  hmops  31992  hmopm  31993  nmcexi  31998  adjlnop  32058  adjmul  32064  adjadd  32065  opsqrlem1  32112  mdsl0  32282  ssmd2  32284  mdexchi  32307  superpos  32326  chrelat2i  32337  atcvatlem  32357  atcvati  32358  chirredlem1  32362  chirredi  32366  atcvat3i  32368  atcvat4i  32369  mdsymlem3  32377  mdsymlem5  32379  cdj3lem2b  32409  ifnebib  32521  isoun  32675  xrge0infss  32735  1arithufdlem3  33503  extdg1id  33671  ddemeas  34241  fsum2dsub  34612  hgt750lemb  34661  bnj1145  34997  subfacp1lem3  35218  subfacp1lem5  35220  cvxpconn  35278  satfv1lem  35398  btwnconn1lem12  36132  colinbtwnle  36152  broutsideof2  36156  lineelsb2  36182  nn0prpwlem  36356  neibastop2lem  36394  tailfb  36411  onsuct0  36475  finxpreclem2  37424  lindsenlbs  37655  poimirlem4  37664  poimirlem26  37686  poimirlem27  37687  poimirlem31  37691  heicant  37695  mblfinlem2  37698  mblfinlem3  37699  ismblfin  37701  ftc1anclem5  37737  ftc1anclem6  37738  ftc1anc  37741  sdclem1  37783  seqpo  37787  sstotbnd  37815  cntotbnd  37836  ismtycnv  37842  ismtyres  37848  heibor  37861  exidreslem  37917  ghomdiv  37932  grpokerinj  37933  rngohomco  38014  rngoisoco  38022  idlsubcl  38063  divrngidl  38068  ispridl2  38078  ispridlc  38110  riotasv3d  38999  omllaw3  39284  omlfh1N  39297  hlrelat2  39442  cvratlem  39460  cvrat  39461  cvrat3  39481  cvrat4  39482  ps-2  39517  elpaddn0  39839  paddss12  39858  pmodlem2  39886  cdleme0cq  40254  cdlemeg49lebilem  40578  cdleme50eq  40580  tendoeq2  40813  tendoex  41014  diameetN  41095  diainN  41096  dvhopN  41155  djajN  41176  dihmeetcl  41384  mapdheq2  41768  3factsumint1  42054  imacrhmcl  42547  psrmnd  42578  evlsvvval  42596  evlselvlem  42619  fsuppind  42623  0prjspn  42661  fphpdo  42850  pell1234qrne0  42886  pell14qrgt0  42892  pell1qrge1  42903  monotoddzzfi  42975  jm2.18  43021  wepwsolem  43075  dnnumch3  43080  dnwech  43081  kelac1  43096  kercvrlsm  43116  onov0suclim  43307  cantnfresb  43357  dssmapnvod  44053  gsumws3  44229  gsumws4  44230  mnuprdlem1  44305  mnuprdlem2  44306  traxext  45010  modelac8prim  45025  cncmpmax  45069  fiiuncl  45102  choicefi  45237  mullimc  45656  mullimcf  45663  idlimc  45666  limclner  45689  climleltrp  45714  limsupub  45742  climuzlem  45781  climliminflimsup2  45847  xlimbr  45865  xlimxrre  45869  dfxlim2v  45885  fperdvper  45957  ioodvbdlimc1lem2  45970  ioodvbdlimc2lem  45972  dvnprodlem1  45984  stoweidlem27  46065  stoweidlem48  46086  fourierdlem42  46187  fourierdlem63  46207  fourierdlem65  46209  dfsalgen2  46379  subsaliuncl  46396  sge0iunmptlemfi  46451  sge0rpcpnf  46459  iundjiun  46498  psmeasure  46509  ovnsubaddlem2  46609  hoidmvle  46638  ovolval4lem2  46688  smflimlem2  46810  smflimlem3  46811  smflimlem6  46814  smflimmpt  46848  fcoresf1  47100  icceuelpart  47467  gpgedgvtx0  48092  gpgedgvtx1  48093  srhmsubcALTV  48356  catprs  49043  thincciso2  49487  functermclem  49539  functermc  49540  fulltermc  49543