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  12508  zmax  12799  xrre  13017  supxr  13161  ixxdisj  13208  iooshf  13272  icodisj  13322  ioojoin  13329  iccshftr  13332  iccshftl  13334  iccdil  13336  icccntr  13338  iccf1o  13342  fzaddel  13404  fzsubel  13406  modadd1  13742  modmul1  13758  seqcaopr  13874  expsub  13945  expmordi  13999  sqlecan  14039  facndiv  14116  hashss  14237  hashfacen  14279  hashfacenOLD  14280  hashf1lem1  14281  hashf1lem1OLD  14282  fi1uzind  14324  brfi1indALT  14327  ccatpfx  14521  swrdccatfn  14544  swrdccatin2  14549  2cshwcshw  14646  resqrex  15070  fprodeq0  15793  lcmdvds  16419  hashdvds  16582  eulerthlem2  16589  pceu  16653  pcqcl  16663  infpnlem1  16717  4sqlem11  16762  ramcl  16836  prmgaplem5  16862  imasvscafn  17354  invfun  17582  initoeu2lem2  17836  catcisolem  17931  funcestrcsetclem8  17970  fullestrcsetc  17974  embedsetcestrclem  17980  funcsetcestrclem8  17985  fullsetcestrc  17989  prfcl  18026  prf1st  18027  prf2nd  18028  1st2ndprf  18029  curfuncf  18062  ipodrsfi  18363  mhmpropd  18543  subsubm  18562  pwsdiagmhm  18576  frmdgsum  18607  grplcan  18743  grplmulf1o  18755  dfgrp3lem  18779  mulgsubcl  18824  subsubg  18884  eqger  18913  resghm  18957  conjghm  18972  orbsta  19026  psgnunilem2  19210  odmulg  19270  sylow2a  19331  sylow3lem1  19339  lsmssv  19355  pj1ghm  19415  frgpup1  19487  ghmplusg  19554  subsubrg  20172  issrngd  20244  lmhmco  20428  lmhmf1o  20431  lmhmima  20432  lmhmpreima  20433  reslmhm  20437  pwsdiaglmhm  20442  pwssplit2  20445  pwssplit3  20446  pj1lmhm  20485  lspdisj  20510  prmirred  20819  cygznlem3  20900  frlmsslsp  21126  frlmlbs  21127  frlmup1  21128  issubassa2  21219  psrbagconf1o  21262  psrbagconf1oOLD  21263  evlslem2  21412  evlslem1  21415  ply1sclf1  21583  mamuass  21672  dmatmul  21769  dmatsubcl  21770  dmatmulcl  21772  dmatcrng  21774  scmatcrng  21793  mdetunilem9  21892  pm2mpghm  22088  fvmptnn04ifb  22123  toponmre  22367  neiptopreu  22407  ordtbas  22466  txcls  22878  txlm  22922  qtoptop2  22973  qtoprest  22991  kqt0lem  23010  ptuncnv  23081  fmfnfmlem4  23231  alexsubALTlem2  23322  tgpmulg  23367  blin  23697  xmeter  23709  xmetresbl  23713  dscmet  23851  nmdvr  23957  metnrmlem3  24147  icccvx  24236  bndth  24244  htpycc  24266  pcohtpylem  24305  pi1blem  24325  lmmbrf  24549  iscfil2  24553  iscau4  24566  minveclem7  24722  elovolm  24762  dyaddisjlem  24882  ismbfd  24926  itg1mulc  24992  dvlip  25280  dvcvx  25307  plypf1  25496  eff1olem  25827  logccv  25941  lawcos  26089  leibpilem1  26213  sqff1o  26454  dvdsppwf1o  26458  dvdsflf1o  26459  fsumdvdsmul  26467  sgmmul  26472  fsumvma  26484  bposlem6  26560  lgsdchr  26626  rpvmasum2  26783  pntpbnd1  26857  ostthlem1  26898  sltres  26933  nodenselem5  26959  nodenselem6  26960  nodense  26963  tgbtwntriv2  27228  ercgrg  27258  hlpasch  27497  colinearalglem4  27657  axlowdimlem15  27704  axcontlem7  27718  axcontlem8  27719  axcontlem10  27721  usgr1v  28003  pthdivtx  28476  clwwlkn1loopb  28786  grpolcan  29271  nvmf  29386  sspmval  29474  nmosetre  29505  minvecolem7  29624  hiassdi  29832  shscli  30058  fh1  30359  fh2  30360  cm2j  30361  chscllem2  30379  spansncvi  30393  5oalem2  30396  adjsym  30574  nmopsetretALT  30604  nmfnsetre  30618  cnvadj  30633  cnvunop  30659  unoplin  30661  hmoplin  30683  lnopmi  30741  hmops  30761  hmopm  30762  nmcexi  30767  adjlnop  30827  adjmul  30833  adjadd  30834  opsqrlem1  30881  mdsl0  31051  ssmd2  31053  mdexchi  31076  superpos  31095  chrelat2i  31106  atcvatlem  31126  atcvati  31127  chirredlem1  31131  chirredi  31135  atcvat3i  31137  atcvat4i  31138  mdsymlem3  31146  mdsymlem5  31148  cdj3lem2b  31178  isoun  31411  xrge0infss  31460  extdg1id  32136  ddemeas  32609  fsum2dsub  32994  hgt750lemb  33043  bnj1145  33379  subfacp1lem3  33550  subfacp1lem5  33552  satfv1lem  33730  sexp2  34182  coflton  34216  addsproplem2  34273  btwnconn1lem12  34579  colinbtwnle  34599  broutsideof2  34603  lineelsb2  34629  nn0prpwlem  34690  neibastop2lem  34728  tailfb  34745  onsuct0  34809  finxpreclem2  35757  lindsenlbs  35969  poimirlem4  35978  poimirlem26  36000  poimirlem27  36001  poimirlem31  36005  heicant  36009  mblfinlem2  36012  mblfinlem3  36013  ismblfin  36015  ftc1anclem5  36051  ftc1anclem6  36052  ftc1anc  36055  sdclem1  36098  seqpo  36102  sstotbnd  36130  cntotbnd  36151  ismtycnv  36157  ismtyres  36163  heibor  36176  exidreslem  36232  ghomdiv  36247  grpokerinj  36248  rngohomco  36329  rngoisoco  36337  idlsubcl  36378  divrngidl  36383  ispridl2  36393  ispridlc  36425  riotasv3d  37318  omllaw3  37603  omlfh1N  37616  hlrelat2  37762  cvratlem  37780  cvrat  37781  cvrat3  37801  cvrat4  37802  ps-2  37837  elpaddn0  38159  paddss12  38178  pmodlem2  38206  cdleme0cq  38574  cdlemeg49lebilem  38898  cdleme50eq  38900  tendoeq2  39133  tendoex  39334  diameetN  39415  diainN  39416  dvhopN  39475  djajN  39496  dihmeetcl  39704  mapdheq2  40088  3factsumint1  40374  metakunt16  40488  evlsbagval  40630  fsuppind  40634  mhphf  40640  0prjspn  40832  fphpdo  41006  pell1234qrne0  41042  pell14qrgt0  41048  pell1qrge1  41059  monotoddzzfi  41132  jm2.18  41178  wepwsolem  41235  dnnumch3  41240  dnwech  41241  kelac1  41256  kercvrlsm  41276  dssmapnvod  42055  gsumws3  42234  gsumws4  42235  mnuprdlem1  42317  mnuprdlem2  42318  cncmpmax  43002  fiiuncl  43038  choicefi  43180  fvelima2  43247  mullimc  43612  mullimcf  43619  idlimc  43622  limclner  43647  climleltrp  43672  limsupub  43700  climuzlem  43739  climliminflimsup2  43805  xlimbr  43823  xlimxrre  43827  dfxlim2v  43843  fperdvper  43915  ioodvbdlimc1lem2  43928  ioodvbdlimc2lem  43930  dvnprodlem1  43942  stoweidlem27  44023  stoweidlem48  44044  fourierdlem42  44145  fourierdlem63  44165  fourierdlem65  44167  dfsalgen2  44337  subsaliuncl  44354  sge0iunmptlemfi  44409  sge0rpcpnf  44417  iundjiun  44456  psmeasure  44467  ovnsubaddlem2  44567  hoidmvle  44596  ovolval4lem2  44646  smflimlem2  44768  smflimlem3  44769  smflimlem6  44772  smflimmpt  44806  fcoresf1  45058  icceuelpart  45383  mgmhmpropd  45834  subsubmgm  45846  srhmsubc  46129  srhmsubcALTV  46147  catprs  46786
  Copyright terms: Public domain W3C validator