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

Theorem adantrl 754
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 479 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 492 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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 197  df-an 385
This theorem is referenced by:  ad2ant2l  799  ad2ant2rl  802  cases2ALT  1035  consensus  1041  3ad2antr2  1181  3ad2antr3  1182  opabssxpd  5481  wfi  5862  ordelord  5894  foco  6274  f1cofveqaeqALT  6667  isocnv  6731  isores2  6734  f1oiso2  6753  offval  7057  ordsucun  7178  xp2nd  7354  1stconst  7421  2ndconst  7422  wfrdmcl  7580  smoord  7619  tfrlem9  7638  tfrlem11  7641  oaass  7798  omordi  7803  omwordri  7809  odi  7816  oewordri  7829  nnawordi  7858  nnmordi  7868  dom2lem  8149  fundmen  8183  sbthlem9  8231  mapen  8277  mapunen  8282  ssenen  8287  domfi  8334  mapfien  8466  inf3lem6  8691  r1val1  8810  rankval3b  8850  numacn  9033  infxpabs  9197  infxp  9200  cfsmolem  9255  infpssrlem4  9291  fin23lem27  9313  isf34lem4  9362  hsmexlem2  9412  axdc3lem2  9436  axdc3lem4  9438  iundom2g  9525  gchen1  9610  fpwwe2lem7  9621  fpwwe2lem11  9625  fpwwe2lem12  9626  prlem936  10032  muladd  10625  leord1  10718  eqord1  10719  ltord2  10720  leord2  10721  eqord2  10722  divadddiv  10903  ltmul12a  11042  lemul12b  11043  supadd  11154  supmullem1  11156  cju  11179  zextlt  11614  zmax  11949  xrre  12164  supxr  12307  ixxdisj  12354  iooshf  12416  icodisj  12461  ioojoin  12467  iccshftr  12470  iccshftl  12472  iccdil  12474  icccntr  12476  iccf1o  12480  fzaddel  12539  fzsubel  12541  modadd1  12872  modmul1  12888  seqcaopr  13003  expsub  13073  sqlecan  13136  facndiv  13240  hashss  13360  hashfacen  13401  hashf1lem1  13402  fi1uzind  13442  brfi1indALT  13445  swrdccatin12lem2b  13657  2cshwcshw  13742  resqrex  14161  fprodeq0  14875  lcmdvds  15494  hashdvds  15653  eulerthlem2  15660  pceu  15724  pcqcl  15734  infpnlem1  15787  4sqlem11  15832  ramcl  15906  prmgaplem5  15932  imasvscafn  16370  invfun  16596  initoeu2lem2  16837  catcisolem  16928  funcestrcsetclem8  16959  fullestrcsetc  16963  embedsetcestrclem  16969  funcsetcestrclem8  16974  fullsetcestrc  16978  prfcl  17015  prf1st  17016  prf2nd  17017  1st2ndprf  17018  curfuncf  17050  ipodrsfi  17335  mhmpropd  17513  subsubm  17529  pwsdiagmhm  17541  gsumccat  17550  frmdgsum  17571  grplcan  17649  grplmulf1o  17661  dfgrp3lem  17685  mulgsubcl  17727  subsubg  17789  eqger  17816  resghm  17848  conjghm  17863  orbsta  17917  psgnunilem2  18086  odmulg  18144  sylow2a  18205  sylow3lem1  18213  lsmssv  18229  pj1ghm  18287  frgpup1  18359  ghmplusg  18420  subsubrg  18979  issrngd  19034  lmhmco  19216  lmhmf1o  19219  lmhmima  19220  lmhmpreima  19221  reslmhm  19225  pwsdiaglmhm  19230  pwssplit2  19233  pwssplit3  19234  pj1lmhm  19273  lspdisj  19298  issubassa2  19518  psrbagconf1o  19547  evlslem2  19685  evlslem1  19688  ply1sclf1  19832  prmirred  20016  cygznlem3  20091  frlmsslsp  20308  frlmlbs  20309  frlmup1  20310  mamuass  20381  dmatmul  20476  dmatsubcl  20477  dmatmulcl  20479  dmatcrng  20481  scmatcrng  20500  mdetunilem9  20599  pm2mpghm  20794  fvmptnn04ifb  20829  toponmre  21070  neiptopreu  21110  ordtbas  21169  txcls  21580  txlm  21624  qtoptop2  21675  qtoprest  21693  kqt0lem  21712  ptuncnv  21783  fmfnfmlem4  21933  alexsubALTlem2  22024  tgpmulg  22069  blin  22398  xmeter  22410  xmetresbl  22414  dscmet  22549  nmdvr  22646  metnrmlem3  22836  icccvx  22921  bndth  22929  htpycc  22951  pcohtpylem  22990  pi1blem  23010  lmmbrf  23231  iscfil2  23235  iscau4  23248  minveclem7  23377  elovolm  23414  dyaddisjlem  23534  ismbfd  23577  itg1mulc  23641  dvlip  23926  dvcvx  23953  plypf1  24138  eff1olem  24464  logccv  24579  lawcos  24716  sqff1o  25078  dvdsppwf1o  25082  dvdsflf1o  25083  fsumdvdsmul  25091  sgmmul  25096  fsumvma  25108  bposlem6  25184  lgsdchr  25250  rpvmasum2  25371  pntpbnd1  25445  ostthlem1  25486  tgbtwntriv2  25552  ercgrg  25582  hlpasch  25818  colhp  25832  colinearalglem4  25959  axlowdimlem15  26006  axcontlem7  26020  axcontlem8  26021  axcontlem10  26023  usgr1v  26318  pthdivtx  26806  clwwlkn1loopb  27143  grpolcan  27664  nvmf  27780  sspmval  27868  nmosetre  27899  sspph  27990  minvecolem7  28019  hiassdi  28228  shscli  28456  fh1  28757  fh2  28758  cm2j  28759  chscllem2  28777  spansncvi  28791  5oalem2  28794  adjsym  28972  nmopsetretALT  29002  nmfnsetre  29016  cnvadj  29031  cnvunop  29057  unoplin  29059  hmoplin  29081  lnopmi  29139  hmops  29159  hmopm  29160  nmcexi  29165  adjlnop  29225  adjmul  29231  adjadd  29232  opsqrlem1  29279  mdsl0  29449  ssmd2  29451  mdexchi  29474  superpos  29493  chrelat2i  29504  atcvatlem  29524  atcvati  29525  chirredlem1  29529  chirredi  29533  atcvat3i  29535  atcvat4i  29536  mdsymlem3  29544  mdsymlem5  29546  cdj3lem2b  29576  isoun  29759  xrge0infss  29805  ddemeas  30579  fsum2dsub  30965  hgt750lemb  31014  bnj1145  31339  subfacp1lem3  31442  subfacp1lem5  31444  frpoind  32017  frind  32020  sltres  32092  nodenselem5  32115  nodenselem6  32116  nodense  32119  btwnconn1lem12  32482  colinbtwnle  32502  broutsideof2  32506  lineelsb2  32532  nn0prpwlem  32594  neibastop2lem  32632  tailfb  32649  onsuct0  32717  finxpreclem2  33509  lindsenlbs  33686  poimirlem4  33695  poimirlem26  33717  poimirlem27  33718  poimirlem31  33722  heicant  33726  mblfinlem2  33729  mblfinlem3  33730  ismblfin  33732  ftc1anclem5  33771  ftc1anclem6  33772  ftc1anc  33775  sdclem1  33821  seqpo  33825  sstotbnd  33856  cntotbnd  33877  ismtycnv  33883  ismtyres  33889  heibor  33902  exidreslem  33958  ghomdiv  33973  grpokerinj  33974  rngohomco  34055  rngoisoco  34063  idlsubcl  34104  divrngidl  34109  ispridl2  34119  ispridlc  34151  riotasv3d  34718  omllaw3  35004  omlfh1N  35017  hlrelat2  35161  cvratlem  35179  cvrat  35180  cvrat3  35200  cvrat4  35201  ps-2  35236  elpaddn0  35558  paddss12  35577  pmodlem2  35605  cdleme0cq  35974  cdlemeg49lebilem  36298  cdleme50eq  36300  tendoeq2  36533  tendoex  36734  diameetN  36816  diainN  36817  dvhopN  36876  djajN  36897  dihmeetcl  37105  mapdheq2  37489  fphpdo  37852  pell1234qrne0  37888  pell14qrgt0  37894  pell1qrge1  37905  monotoddzzfi  37978  expmordi  37983  jm2.18  38026  wepwsolem  38083  dnnumch3  38088  dnwech  38089  kelac1  38104  kercvrlsm  38124  dssmapnvod  38785  gsumws3  38970  gsumws4  38971  cncmpmax  39659  fiiuncl  39702  choicefi  39860  fvelima2  39943  mullimc  40320  mullimcf  40327  idlimc  40330  limclner  40355  climleltrp  40380  limsupub  40408  climuzlem  40447  climliminflimsup2  40513  xlimbr  40525  xlimxrre  40529  dfxlim2v  40545  fperdvper  40605  ioodvbdlimc1lem2  40619  ioodvbdlimc2lem  40621  dvnprodlem1  40633  stoweidlem27  40716  stoweidlem48  40737  fourierdlem42  40838  fourierdlem63  40858  fourierdlem65  40860  dfsalgen2  41031  subsaliuncl  41048  sge0iunmptlemfi  41102  sge0rpcpnf  41110  iundjiun  41149  psmeasure  41160  ovnsubaddlem2  41260  hoidmvle  41289  ovolval4lem2  41339  ovolval5lem3  41343  smflimlem2  41455  smflimlem3  41456  smflimlem6  41459  smflimmpt  41491  icceuelpart  41851  mgmhmpropd  42264  subsubmgm  42276  srhmsubc  42555  srhmsubcALTV  42573
  Copyright terms: Public domain W3C validator