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

Theorem adantrl 698
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 473 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 582 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  ad2ant2l  743  ad2ant2rl  746  cases2ALT  1062  consensus  1068  3ad2antr2  1233  3ad2antr3  1234  opabssxpd  5539  wfi  5926  ordelord  5958  foco  6341  f1cofveqaeqALT  6740  isocnv  6804  isores2  6807  f1oiso2  6826  offval  7134  ordsucun  7255  xp2nd  7431  1stconst  7499  2ndconst  7500  wfrdmcl  7659  smoord  7698  tfrlem9  7717  tfrlem11  7720  oaass  7878  omordi  7883  omwordri  7889  odi  7896  oewordri  7909  nnawordi  7938  nnmordi  7948  dom2lem  8232  fundmen  8266  sbthlem9  8317  mapen  8363  mapunen  8368  ssenen  8373  domfi  8420  mapfien  8552  inf3lem6  8777  r1val1  8896  rankval3b  8936  numacn  9155  infxpabs  9319  infxp  9322  cfsmolem  9377  infpssrlem4  9413  fin23lem27  9435  isf34lem4  9484  hsmexlem2  9534  axdc3lem2  9558  axdc3lem4  9560  iundom2g  9647  gchen1  9732  fpwwe2lem7  9743  fpwwe2lem11  9747  fpwwe2lem12  9748  prlem936  10154  muladd  10747  leord1  10840  eqord1  10841  ltord2  10842  leord2  10843  eqord2  10844  divadddiv  11025  ltmul12a  11164  lemul12b  11165  supadd  11276  supmullem1  11278  cju  11301  zextlt  11717  zmax  12004  xrre  12218  supxr  12361  ixxdisj  12408  iooshf  12470  icodisj  12518  ioojoin  12526  iccshftr  12529  iccshftl  12531  iccdil  12533  icccntr  12535  iccf1o  12539  fzaddel  12598  fzsubel  12600  modadd1  12931  modmul1  12947  seqcaopr  13061  expsub  13131  sqlecan  13194  facndiv  13295  hashss  13414  hashfacen  13455  hashf1lem1  13456  fi1uzind  13496  brfi1indALT  13499  swrdccatin12lem2b  13710  2cshwcshw  13795  resqrex  14214  fprodeq0  14926  lcmdvds  15540  hashdvds  15697  eulerthlem2  15704  pceu  15768  pcqcl  15778  infpnlem1  15831  4sqlem11  15876  ramcl  15950  prmgaplem5  15976  imasvscafn  16402  invfun  16628  initoeu2lem2  16869  catcisolem  16960  funcestrcsetclem8  16992  fullestrcsetc  16996  embedsetcestrclem  17002  funcsetcestrclem8  17007  fullsetcestrc  17011  prfcl  17048  prf1st  17049  prf2nd  17050  1st2ndprf  17051  curfuncf  17083  ipodrsfi  17368  mhmpropd  17546  subsubm  17562  pwsdiagmhm  17574  gsumccat  17583  frmdgsum  17604  grplcan  17682  grplmulf1o  17694  dfgrp3lem  17718  mulgsubcl  17760  subsubg  17819  eqger  17846  resghm  17878  conjghm  17893  orbsta  17947  psgnunilem2  18116  odmulg  18174  sylow2a  18235  sylow3lem1  18243  lsmssv  18259  pj1ghm  18317  frgpup1  18389  ghmplusg  18450  subsubrg  19010  issrngd  19065  lmhmco  19250  lmhmf1o  19253  lmhmima  19254  lmhmpreima  19255  reslmhm  19259  pwsdiaglmhm  19264  pwssplit2  19267  pwssplit3  19268  pj1lmhm  19307  lspdisj  19332  issubassa2  19554  psrbagconf1o  19583  evlslem2  19720  evlslem1  19723  ply1sclf1  19867  prmirred  20051  cygznlem3  20125  frlmsslsp  20345  frlmlbs  20346  frlmup1  20347  mamuass  20418  dmatmul  20514  dmatsubcl  20515  dmatmulcl  20517  dmatcrng  20519  scmatcrng  20538  mdetunilem9  20637  pm2mpghm  20834  fvmptnn04ifb  20869  toponmre  21111  neiptopreu  21151  ordtbas  21210  txcls  21621  txlm  21665  qtoptop2  21716  qtoprest  21734  kqt0lem  21753  ptuncnv  21824  fmfnfmlem4  21974  alexsubALTlem2  22065  tgpmulg  22110  blin  22439  xmeter  22451  xmetresbl  22455  dscmet  22590  nmdvr  22687  metnrmlem3  22877  icccvx  22962  bndth  22970  htpycc  22992  pcohtpylem  23031  pi1blem  23051  lmmbrf  23272  iscfil2  23276  iscau4  23289  minveclem7  23418  elovolm  23456  dyaddisjlem  23576  ismbfd  23620  itg1mulc  23685  dvlip  23970  dvcvx  23997  plypf1  24182  eff1olem  24509  logccv  24623  lawcos  24760  sqff1o  25122  dvdsppwf1o  25126  dvdsflf1o  25127  fsumdvdsmul  25135  sgmmul  25140  fsumvma  25152  bposlem6  25228  lgsdchr  25294  rpvmasum2  25415  pntpbnd1  25489  ostthlem1  25530  tgbtwntriv2  25596  ercgrg  25626  hlpasch  25862  colhp  25876  colinearalglem4  26003  axlowdimlem15  26050  axcontlem7  26064  axcontlem8  26065  axcontlem10  26067  usgr1v  26364  pthdivtx  26853  clwwlkn1loopb  27192  grpolcan  27713  nvmf  27828  sspmval  27916  nmosetre  27947  sspph  28038  minvecolem7  28067  hiassdi  28276  shscli  28504  fh1  28805  fh2  28806  cm2j  28807  chscllem2  28825  spansncvi  28839  5oalem2  28842  adjsym  29020  nmopsetretALT  29050  nmfnsetre  29064  cnvadj  29079  cnvunop  29105  unoplin  29107  hmoplin  29129  lnopmi  29187  hmops  29207  hmopm  29208  nmcexi  29213  adjlnop  29273  adjmul  29279  adjadd  29280  opsqrlem1  29327  mdsl0  29497  ssmd2  29499  mdexchi  29522  superpos  29541  chrelat2i  29552  atcvatlem  29572  atcvati  29573  chirredlem1  29577  chirredi  29581  atcvat3i  29583  atcvat4i  29584  mdsymlem3  29592  mdsymlem5  29594  cdj3lem2b  29624  isoun  29806  xrge0infss  29852  ddemeas  30624  fsum2dsub  31010  hgt750lemb  31059  bnj1145  31384  subfacp1lem3  31487  subfacp1lem5  31489  frpoind  32061  frind  32064  sltres  32136  nodenselem5  32159  nodenselem6  32160  nodense  32163  btwnconn1lem12  32526  colinbtwnle  32546  broutsideof2  32550  lineelsb2  32576  nn0prpwlem  32638  neibastop2lem  32676  tailfb  32693  onsuct0  32757  finxpreclem2  33543  cnfinltrel  33557  lindsenlbs  33717  poimirlem4  33726  poimirlem26  33748  poimirlem27  33749  poimirlem31  33753  heicant  33757  mblfinlem2  33760  mblfinlem3  33761  ismblfin  33763  ftc1anclem5  33801  ftc1anclem6  33802  ftc1anc  33805  sdclem1  33850  seqpo  33854  sstotbnd  33885  cntotbnd  33906  ismtycnv  33912  ismtyres  33918  heibor  33931  exidreslem  33987  ghomdiv  34002  grpokerinj  34003  rngohomco  34084  rngoisoco  34092  idlsubcl  34133  divrngidl  34138  ispridl2  34148  ispridlc  34180  riotasv3d  34739  omllaw3  35025  omlfh1N  35038  hlrelat2  35183  cvratlem  35201  cvrat  35202  cvrat3  35222  cvrat4  35223  ps-2  35258  elpaddn0  35580  paddss12  35599  pmodlem2  35627  cdleme0cq  35996  cdlemeg49lebilem  36320  cdleme50eq  36322  tendoeq2  36555  tendoex  36756  diameetN  36837  diainN  36838  dvhopN  36897  djajN  36918  dihmeetcl  37126  mapdheq2  37510  fphpdo  37883  pell1234qrne0  37919  pell14qrgt0  37925  pell1qrge1  37936  monotoddzzfi  38008  expmordi  38013  jm2.18  38056  wepwsolem  38113  dnnumch3  38118  dnwech  38119  kelac1  38134  kercvrlsm  38154  dssmapnvod  38814  gsumws3  38999  gsumws4  39000  cncmpmax  39685  fiiuncl  39727  choicefi  39879  fvelima2  39958  mullimc  40328  mullimcf  40335  idlimc  40338  limclner  40363  climleltrp  40388  limsupub  40416  climuzlem  40455  climliminflimsup2  40521  xlimbr  40533  xlimxrre  40537  dfxlim2v  40553  fperdvper  40613  ioodvbdlimc1lem2  40627  ioodvbdlimc2lem  40629  dvnprodlem1  40641  stoweidlem27  40723  stoweidlem48  40744  fourierdlem42  40845  fourierdlem63  40865  fourierdlem65  40867  dfsalgen2  41038  subsaliuncl  41055  sge0iunmptlemfi  41109  sge0rpcpnf  41117  iundjiun  41156  psmeasure  41167  ovnsubaddlem2  41267  hoidmvle  41296  ovolval4lem2  41346  ovolval5lem3  41350  smflimlem2  41462  smflimlem3  41463  smflimlem6  41466  smflimmpt  41498  icceuelpart  41947  mgmhmpropd  42353  subsubmgm  42365  srhmsubc  42644  srhmsubcALTV  42662
  Copyright terms: Public domain W3C validator