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

Theorem adantrl 715
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
StepHypRef Expression
1 simpr 486 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 594 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397
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 206  df-an 398
This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  cases2ALT  1048  consensus  1052  3ad2antr2  1190  3ad2antr3  1191  po2ne  5559  opabssxpd  5676  frpoind  6293  wfiOLD  6302  ordelord  6336  f1un  6800  f1cofveqaeqALT  7201  isocnv  7270  isores2  7273  f1oiso2  7292  offval  7617  ordsucun  7751  xp2nd  7945  2ndconst  8022  wfrdmclOLD  8231  smoord  8279  tfrlem9  8299  tfrlem11  8302  oaass  8476  omordi  8481  omwordri  8487  odi  8494  oewordri  8507  nnawordi  8536  nnmordi  8546  dom2lem  8866  fundmen  8909  sbthlem9  8969  mapen  9019  mapunen  9024  ssenen  9029  domfi  9070  mapfien  9278  inf3lem6  9503  ttrclselem2  9596  frind  9620  r1val1  9656  rankval3b  9696  numacn  9919  infxpabs  10082  infxp  10085  cfsmolem  10140  infpssrlem4  10176  fin23lem27  10198  isf34lem4  10247  hsmexlem2  10297  axdc3lem2  10321  axdc3lem4  10323  iundom2g  10410  gchen1  10495  fpwwe2lem6  10506  fpwwe2lem10  10510  fpwwe2lem11  10511  prlem936  10917  muladd  11521  leord1  11616  eqord1  11617  ltord2  11618  leord2  11619  eqord2  11620  divadddiv  11804  ltmul12a  11945  lemul12b  11946  fimaxre  12033  supadd  12057  supmullem1  12059  cju  12083  zextlt  12511  zmax  12800  xrre  13018  supxr  13162  ixxdisj  13209  iooshf  13273  icodisj  13323  ioojoin  13330  iccshftr  13333  iccshftl  13335  iccdil  13337  icccntr  13339  iccf1o  13343  fzaddel  13405  fzsubel  13407  modadd1  13743  modmul1  13759  seqcaopr  13875  expsub  13946  expmordi  14000  sqlecan  14040  facndiv  14117  hashss  14238  hashfacen  14280  hashfacenOLD  14281  hashf1lem1  14282  hashf1lem1OLD  14283  fi1uzind  14325  brfi1indALT  14328  ccatpfx  14522  swrdccatfn  14545  swrdccatin2  14550  2cshwcshw  14647  resqrex  15071  fprodeq0  15794  lcmdvds  16420  hashdvds  16583  eulerthlem2  16590  pceu  16654  pcqcl  16664  infpnlem1  16718  4sqlem11  16763  ramcl  16837  prmgaplem5  16863  imasvscafn  17355  invfun  17583  initoeu2lem2  17837  catcisolem  17932  funcestrcsetclem8  17971  fullestrcsetc  17975  embedsetcestrclem  17981  funcsetcestrclem8  17986  fullsetcestrc  17990  prfcl  18027  prf1st  18028  prf2nd  18029  1st2ndprf  18030  curfuncf  18063  ipodrsfi  18364  mhmpropd  18544  subsubm  18563  pwsdiagmhm  18577  frmdgsum  18608  grplcan  18744  grplmulf1o  18756  dfgrp3lem  18780  mulgsubcl  18825  subsubg  18886  eqger  18915  resghm  18959  conjghm  18974  orbsta  19028  psgnunilem2  19212  odmulg  19273  sylow2a  19336  sylow3lem1  19344  lsmssv  19360  pj1ghm  19420  frgpup1  19492  ghmplusg  19559  subsubrg  20177  issrngd  20249  lmhmco  20433  lmhmf1o  20436  lmhmima  20437  lmhmpreima  20438  reslmhm  20442  pwsdiaglmhm  20447  pwssplit2  20450  pwssplit3  20451  pj1lmhm  20490  lspdisj  20515  prmirred  20824  cygznlem3  20905  frlmsslsp  21131  frlmlbs  21132  frlmup1  21133  issubassa2  21224  psrbagconf1o  21267  psrbagconf1oOLD  21268  evlslem2  21417  evlslem1  21420  ply1sclf1  21588  mamuass  21677  dmatmul  21774  dmatsubcl  21775  dmatmulcl  21777  dmatcrng  21779  scmatcrng  21798  mdetunilem9  21897  pm2mpghm  22093  fvmptnn04ifb  22128  toponmre  22372  neiptopreu  22412  ordtbas  22471  txcls  22883  txlm  22927  qtoptop2  22978  qtoprest  22996  kqt0lem  23015  ptuncnv  23086  fmfnfmlem4  23236  alexsubALTlem2  23327  tgpmulg  23372  blin  23702  xmeter  23714  xmetresbl  23718  dscmet  23856  nmdvr  23962  metnrmlem3  24152  icccvx  24241  bndth  24249  htpycc  24271  pcohtpylem  24310  pi1blem  24330  lmmbrf  24554  iscfil2  24558  iscau4  24571  minveclem7  24727  elovolm  24767  dyaddisjlem  24887  ismbfd  24931  itg1mulc  24997  dvlip  25285  dvcvx  25312  plypf1  25501  eff1olem  25832  logccv  25946  lawcos  26094  leibpilem1  26218  sqff1o  26459  dvdsppwf1o  26463  dvdsflf1o  26464  fsumdvdsmul  26472  sgmmul  26477  fsumvma  26489  bposlem6  26565  lgsdchr  26631  rpvmasum2  26788  pntpbnd1  26862  ostthlem1  26903  sltres  26938  nodenselem5  26964  nodenselem6  26965  nodense  26968  tgbtwntriv2  27234  ercgrg  27264  hlpasch  27503  colinearalglem4  27663  axlowdimlem15  27710  axcontlem7  27724  axcontlem8  27725  axcontlem10  27727  usgr1v  28009  pthdivtx  28482  clwwlkn1loopb  28792  grpolcan  29277  nvmf  29392  sspmval  29480  nmosetre  29511  minvecolem7  29630  hiassdi  29838  shscli  30064  fh1  30365  fh2  30366  cm2j  30367  chscllem2  30385  spansncvi  30399  5oalem2  30402  adjsym  30580  nmopsetretALT  30610  nmfnsetre  30624  cnvadj  30639  cnvunop  30665  unoplin  30667  hmoplin  30689  lnopmi  30747  hmops  30767  hmopm  30768  nmcexi  30773  adjlnop  30833  adjmul  30839  adjadd  30840  opsqrlem1  30887  mdsl0  31057  ssmd2  31059  mdexchi  31082  superpos  31101  chrelat2i  31112  atcvatlem  31132  atcvati  31133  chirredlem1  31137  chirredi  31141  atcvat3i  31143  atcvat4i  31144  mdsymlem3  31152  mdsymlem5  31154  cdj3lem2b  31184  isoun  31417  xrge0infss  31466  extdg1id  32142  ddemeas  32615  fsum2dsub  33000  hgt750lemb  33049  bnj1145  33385  subfacp1lem3  33556  subfacp1lem5  33558  satfv1lem  33736  sexp2  34185  coflton  34220  addsproplem2  34278  btwnconn1lem12  34614  colinbtwnle  34634  broutsideof2  34638  lineelsb2  34664  nn0prpwlem  34725  neibastop2lem  34763  tailfb  34780  onsuct0  34844  finxpreclem2  35792  lindsenlbs  36004  poimirlem4  36013  poimirlem26  36035  poimirlem27  36036  poimirlem31  36040  heicant  36044  mblfinlem2  36047  mblfinlem3  36048  ismblfin  36050  ftc1anclem5  36086  ftc1anclem6  36087  ftc1anc  36090  sdclem1  36133  seqpo  36137  sstotbnd  36165  cntotbnd  36186  ismtycnv  36192  ismtyres  36198  heibor  36211  exidreslem  36267  ghomdiv  36282  grpokerinj  36283  rngohomco  36364  rngoisoco  36372  idlsubcl  36413  divrngidl  36418  ispridl2  36428  ispridlc  36460  riotasv3d  37353  omllaw3  37638  omlfh1N  37651  hlrelat2  37797  cvratlem  37815  cvrat  37816  cvrat3  37836  cvrat4  37837  ps-2  37872  elpaddn0  38194  paddss12  38213  pmodlem2  38241  cdleme0cq  38609  cdlemeg49lebilem  38933  cdleme50eq  38935  tendoeq2  39168  tendoex  39369  diameetN  39450  diainN  39451  dvhopN  39510  djajN  39531  dihmeetcl  39739  mapdheq2  40123  3factsumint1  40409  metakunt16  40523  evlsbagval  40663  fsuppind  40667  mhphf  40673  0prjspn  40868  fphpdo  41042  pell1234qrne0  41078  pell14qrgt0  41084  pell1qrge1  41095  monotoddzzfi  41168  jm2.18  41214  wepwsolem  41271  dnnumch3  41276  dnwech  41277  kelac1  41292  kercvrlsm  41312  dssmapnvod  42091  gsumws3  42270  gsumws4  42271  mnuprdlem1  42353  mnuprdlem2  42354  cncmpmax  43038  fiiuncl  43074  choicefi  43216  fvelima2  43283  mullimc  43648  mullimcf  43655  idlimc  43658  limclner  43683  climleltrp  43708  limsupub  43736  climuzlem  43775  climliminflimsup2  43841  xlimbr  43859  xlimxrre  43863  dfxlim2v  43879  fperdvper  43951  ioodvbdlimc1lem2  43964  ioodvbdlimc2lem  43966  dvnprodlem1  43978  stoweidlem27  44059  stoweidlem48  44080  fourierdlem42  44181  fourierdlem63  44201  fourierdlem65  44203  dfsalgen2  44373  subsaliuncl  44390  sge0iunmptlemfi  44445  sge0rpcpnf  44453  iundjiun  44492  psmeasure  44503  ovnsubaddlem2  44603  hoidmvle  44632  ovolval4lem2  44682  smflimlem2  44804  smflimlem3  44805  smflimlem6  44808  smflimmpt  44842  fcoresf1  45094  icceuelpart  45419  mgmhmpropd  45870  subsubmgm  45882  srhmsubc  46165  srhmsubcALTV  46183  catprs  46822
  Copyright terms: Public domain W3C validator