MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  adantrl Structured version   Visualization version   Unicode version

Theorem adantrl 727
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  |-  ( (
ph  /\  ps )  ->  ch )
Assertion
Ref Expression
adantrl  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )

Proof of Theorem adantrl
StepHypRef Expression
1 simpr 467 . 2  |-  ( ( th  /\  ps )  ->  ps )
2 adant2.1 . 2  |-  ( (
ph  /\  ps )  ->  ch )
31, 2sylan2 481 1  |-  ( (
ph  /\  ( th  /\  ps ) )  ->  ch )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 375
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 190  df-an 377
This theorem is referenced by:  ad2ant2l  757  ad2ant2rl  760  consensus  976  cases2  989  3ad2antr2  1180  3ad2antr3  1181  wfi  5436  ordelord  5468  foco  5830  isocnv  6251  isores2  6254  f1oiso2  6273  offval  6570  ordsucun  6684  opabex2  6763  xp2nd  6856  1stconst  6916  2ndconst  6917  wfrdmcl  7075  smoord  7115  tfrlem9  7134  tfrlem11  7137  oaass  7293  omordi  7298  omwordri  7304  odi  7311  oewordri  7324  nnawordi  7353  nnmordi  7363  dom2lem  7640  fundmen  7674  sbthlem9  7721  mapen  7767  mapunen  7772  ssenen  7777  domfi  7824  mapfien  7952  inf3lem6  8169  r1val1  8288  rankval3b  8328  numacn  8511  infxpabs  8673  infxp  8676  cfsmolem  8731  infpssrlem4  8767  fin23lem27  8789  isf34lem4  8838  hsmexlem2  8888  axdc3lem2  8912  axdc3lem4  8914  iundom2g  8996  gchen1  9081  fpwwe2lem7  9092  fpwwe2lem11  9096  fpwwe2lem12  9097  prlem936  9503  muladd  10084  leord1  10174  eqord1  10175  ltord2  10176  leord2  10177  eqord2  10178  divadddiv  10355  ltmul12a  10494  lemul12b  10495  supadd  10608  supmullem1  10610  cju  10638  zextlt  11044  zmax  11295  xrre  11498  supxr  11632  ixxdisj  11684  iooshf  11747  icodisj  11792  ioojoin  11798  iccshftr  11801  iccshftl  11803  iccdil  11805  icccntr  11807  iccf1o  11811  fzaddel  11868  fzsubel  11869  modadd1  12172  modmul1  12181  seqcaopr  12288  expsub  12358  sqlecan  12419  facndiv  12511  hashss  12624  hashfacen  12656  hashf1lem1  12657  fi1uzind  12689  brfi1indALT  12692  swrdccatin12lem2b  12885  2cshwcshw  12967  resqrex  13369  fprodeq0  14084  lcmdvds  14628  hashdvds  14778  eulerthlem2  14785  pceu  14851  pcqcl  14861  infpnlem1  14909  4sqlem11  14954  ramcl  15042  prmgaplem5  15080  imasvscafn  15498  invfun  15724  initoeu2lem2  15965  catcisolem  16056  funcestrcsetclem8  16087  fullestrcsetc  16091  embedsetcestrclem  16097  funcsetcestrclem8  16102  fullsetcestrc  16106  prfcl  16143  prf1st  16144  prf2nd  16145  1st2ndprf  16146  curfuncf  16178  ipodrsfi  16464  mhmpropd  16643  subsubm  16659  pwsdiagmhm  16671  gsumccat  16680  frmdgsum  16701  grplcan  16773  grplmulf1o  16783  mulgsubcl  16827  subsubg  16895  eqger  16922  resghm  16954  conjghm  16968  orbsta  17022  psgnunilem2  17191  odmulg  17262  sylow2a  17326  sylow3lem1  17334  lsmssv  17350  pj1ghm  17408  frgpup1  17480  ghmplusg  17539  subsubrg  18089  issrngd  18144  lmhmco  18321  lmhmf1o  18324  lmhmima  18325  lmhmpreima  18326  reslmhm  18330  pwsdiaglmhm  18335  pwssplit2  18338  pwssplit3  18339  pj1lmhm  18378  lspdisj  18403  issubassa2  18624  psrbagconf1o  18653  evlslem2  18790  evlslem1  18793  ply1sclf1  18937  prmirred  19121  cygznlem3  19195  frlmsslsp  19409  frlmlbs  19410  frlmup1  19411  mamuass  19482  dmatmul  19577  dmatsubcl  19578  dmatmulcl  19580  dmatcrng  19582  scmatcrng  19601  mdetunilem9  19700  pm2mpghm  19895  fvmptnn04ifb  19930  toponmre  20164  neiptopreu  20204  ordtbas  20263  txcls  20674  txlm  20718  qtoptop2  20769  qtoprest  20787  kqt0lem  20806  ptuncnv  20877  fmfnfmlem4  21027  alexsubALTlem2  21118  tgpmulg  21163  blin  21491  xmeter  21503  xmetresbl  21507  dscmet  21642  nmdvr  21728  metnrmlem3  21933  metnrmlem3OLD  21948  icccvx  22033  bndth  22041  htpycc  22066  pcohtpylem  22105  pi1blem  22125  lmmbrf  22287  iscfil2  22291  iscau4  22304  minveclem7  22432  minveclem7OLD  22444  elovolm  22483  dyaddisjlem  22609  ismbfd  22652  itg1mulc  22718  dvlip  23001  dvcvx  23028  plypf1  23222  eff1olem  23553  logccv  23664  lawcos  23801  sqff1o  24165  dvdsppwf1o  24171  dvdsflf1o  24172  fsumdvdsmul  24180  sgmmul  24185  fsumvma  24197  bposlem6  24273  lgsdchr  24332  rpvmasum2  24406  pntpbnd1  24480  ostthlem1  24521  tgbtwntriv2  24587  ercgrg  24618  hlpasch  24854  colhp  24868  colinearalglem4  24995  axlowdimlem15  25042  axcontlem7  25056  axcontlem8  25057  axcontlem10  25059  spthonepeq  25373  usgra2adedgspth  25397  usgra2adedgwlk  25398  usgra2adedgwlkon  25399  numclwlk1lem2f1  25878  grpolcan  26017  isgrp2d  26019  nvmf  26323  nvsubadd  26332  sspmval  26428  sspival  26433  nmosetre  26461  sspph  26552  minvecolem7  26581  minvecolem7OLD  26591  hiassdi  26800  shscli  27026  fh1  27327  fh2  27328  cm2j  27329  chscllem2  27347  spansncvi  27361  5oalem2  27364  adjsym  27542  nmopsetretALT  27572  nmfnsetre  27586  cnvadj  27601  cnvunop  27627  unoplin  27629  hmoplin  27651  lnopmi  27709  hmops  27729  hmopm  27730  nmcexi  27735  adjlnop  27795  adjmul  27801  adjadd  27802  opsqrlem1  27849  mdsl0  28019  ssmd2  28021  mdexchi  28044  superpos  28063  chrelat2i  28074  atcvatlem  28094  atcvati  28095  chirredlem1  28099  chirredi  28103  atcvat3i  28105  atcvat4i  28106  mdsymlem3  28114  mdsymlem5  28116  cdj3lem2b  28146  isoun  28334  xrge0infss  28392  xrge0infssOLD  28393  ddemeas  29109  bnj1145  29852  subfacp1lem3  29955  subfacp1lem5  29957  ghomf1olem  30362  frind  30531  sltres  30601  nodenselem6  30625  nodenselem7  30626  nodense  30628  nofulllem5  30645  btwnconn1lem12  30915  colinbtwnle  30935  broutsideof2  30939  lineelsb2  30965  nn0prpwlem  31028  neibastop2lem  31066  tailfb  31083  onsuct0  31151  finxpreclem2  31828  poimirlem4  31990  poimirlem26  32012  poimirlem27  32013  poimirlem31  32017  heicant  32021  mblfinlem2  32024  mblfinlem3  32025  ismblfin  32027  ftc1anclem5  32067  ftc1anclem6  32068  ftc1anc  32071  sdclem1  32118  seqpo  32122  sstotbnd  32153  cntotbnd  32174  ismtycnv  32180  ismtyres  32186  heibor  32199  exidreslem  32221  ghomdiv  32228  grpokerinj  32229  rngohomco  32259  rngoisoco  32267  idlsubcl  32302  divrngidl  32307  ispridl2  32317  ispridlc  32349  riotasv3d  32578  omllaw3  32857  omlfh1N  32870  hlrelat2  33014  cvratlem  33032  cvrat  33033  cvrat3  33053  cvrat4  33054  ps-2  33089  elpaddn0  33411  paddss12  33430  pmodlem2  33458  cdleme0cq  33827  cdlemeg49lebilem  34152  cdleme50eq  34154  tendoeq2  34387  tendoex  34588  diameetN  34670  diainN  34671  dvhopN  34730  djajN  34751  dihmeetcl  34959  mapdheq2  35343  fphpdo  35706  pell1234qrne0  35745  pell14qrgt0  35751  pell1qrge1  35762  monotoddzzfi  35836  expmordi  35841  jm2.18  35889  wepwsolem  35946  dnnumch3  35951  dnwech  35952  kelac1  35967  kercvrlsm  35987  gsumws3  36693  gsumws4  36694  cncmpmax  37394  fiiuncl  37445  choicefi  37535  mullimc  37782  mullimcf  37789  idlimc  37792  limclner  37818  fperdvper  37876  ioodvbdlimc1lem2  37890  ioodvbdlimc1lem2OLD  37892  ioodvbdlimc2lem  37894  ioodvbdlimc2lemOLD  37895  dvnprodlem1  37907  stoweidlem27  37988  stoweidlem48  38010  fourierdlem42  38113  fourierdlem42OLD  38114  fourierdlem63  38134  fourierdlem65  38136  dfsalgen2  38301  sge0iunmptlemfi  38358  sge0rpcpnf  38366  iundjiun  38403  psmeasure  38414  ovnsubaddlem2  38500  hoidmvle  38529  ovolval4lem2  38579  ovolval5lem3  38583  icceuelpart  38885  f1cofveqaeqALT  39152  pthdivtx  39858  usgra2adedglem1  40039  mgmhmpropd  40154  subsubmgm  40166  srhmsubc  40447  srhmsubcALTV  40466
  Copyright terms: Public domain W3C validator