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

Theorem adantrl 751
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 477 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 491 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 197  df-an 386
This theorem is referenced by:  ad2ant2l  781  ad2ant2rl  784  cases2  992  consensus  998  3ad2antr2  1225  3ad2antr3  1226  opabssxpd  5327  wfi  5701  ordelord  5733  foco  6112  f1cofveqaeqALT  6501  isocnv  6565  isores2  6568  f1oiso2  6587  offval  6889  ordsucun  7010  xp2nd  7184  1stconst  7250  2ndconst  7251  wfrdmcl  7408  smoord  7447  tfrlem9  7466  tfrlem11  7469  oaass  7626  omordi  7631  omwordri  7637  odi  7644  oewordri  7657  nnawordi  7686  nnmordi  7696  dom2lem  7980  fundmen  8015  sbthlem9  8063  mapen  8109  mapunen  8114  ssenen  8119  domfi  8166  mapfien  8298  inf3lem6  8515  r1val1  8634  rankval3b  8674  numacn  8857  infxpabs  9019  infxp  9022  cfsmolem  9077  infpssrlem4  9113  fin23lem27  9135  isf34lem4  9184  hsmexlem2  9234  axdc3lem2  9258  axdc3lem4  9260  iundom2g  9347  gchen1  9432  fpwwe2lem7  9443  fpwwe2lem11  9447  fpwwe2lem12  9448  prlem936  9854  muladd  10447  leord1  10540  eqord1  10541  ltord2  10542  leord2  10543  eqord2  10544  divadddiv  10725  ltmul12a  10864  lemul12b  10865  supadd  10976  supmullem1  10978  cju  11001  zextlt  11436  zmax  11770  xrre  11985  supxr  12128  ixxdisj  12175  iooshf  12237  icodisj  12282  ioojoin  12288  iccshftr  12291  iccshftl  12293  iccdil  12295  icccntr  12297  iccf1o  12301  fzaddel  12360  fzsubel  12362  modadd1  12690  modmul1  12706  seqcaopr  12821  expsub  12891  sqlecan  12954  facndiv  13058  hashss  13180  hashfacen  13221  hashf1lem1  13222  fi1uzind  13262  brfi1indALT  13265  fi1uzindOLD  13268  brfi1indALTOLD  13271  swrdccatin12lem2b  13467  2cshwcshw  13552  resqrex  13972  fprodeq0  14686  lcmdvds  15302  hashdvds  15461  eulerthlem2  15468  pceu  15532  pcqcl  15542  infpnlem1  15595  4sqlem11  15640  ramcl  15714  prmgaplem5  15740  imasvscafn  16178  invfun  16405  initoeu2lem2  16646  catcisolem  16737  funcestrcsetclem8  16768  fullestrcsetc  16772  embedsetcestrclem  16778  funcsetcestrclem8  16783  fullsetcestrc  16787  prfcl  16824  prf1st  16825  prf2nd  16826  1st2ndprf  16827  curfuncf  16859  ipodrsfi  17144  mhmpropd  17322  subsubm  17338  pwsdiagmhm  17350  gsumccat  17359  frmdgsum  17380  grplcan  17458  grplmulf1o  17470  dfgrp3lem  17494  mulgsubcl  17536  subsubg  17598  eqger  17625  resghm  17657  conjghm  17672  orbsta  17727  psgnunilem2  17896  odmulg  17954  sylow2a  18015  sylow3lem1  18023  lsmssv  18039  pj1ghm  18097  frgpup1  18169  ghmplusg  18230  subsubrg  18787  issrngd  18842  lmhmco  19024  lmhmf1o  19027  lmhmima  19028  lmhmpreima  19029  reslmhm  19033  pwsdiaglmhm  19038  pwssplit2  19041  pwssplit3  19042  pj1lmhm  19081  lspdisj  19106  issubassa2  19326  psrbagconf1o  19355  evlslem2  19493  evlslem1  19496  ply1sclf1  19640  prmirred  19824  cygznlem3  19899  frlmsslsp  20116  frlmlbs  20117  frlmup1  20118  mamuass  20189  dmatmul  20284  dmatsubcl  20285  dmatmulcl  20287  dmatcrng  20289  scmatcrng  20308  mdetunilem9  20407  pm2mpghm  20602  fvmptnn04ifb  20637  toponmre  20878  neiptopreu  20918  ordtbas  20977  txcls  21388  txlm  21432  qtoptop2  21483  qtoprest  21501  kqt0lem  21520  ptuncnv  21591  fmfnfmlem4  21742  alexsubALTlem2  21833  tgpmulg  21878  blin  22207  xmeter  22219  xmetresbl  22223  dscmet  22358  nmdvr  22455  metnrmlem3  22645  icccvx  22730  bndth  22738  htpycc  22760  pcohtpylem  22800  pi1blem  22820  lmmbrf  23041  iscfil2  23045  iscau4  23058  minveclem7  23187  elovolm  23224  dyaddisjlem  23344  ismbfd  23388  itg1mulc  23452  dvlip  23737  dvcvx  23764  plypf1  23949  eff1olem  24275  logccv  24390  lawcos  24527  sqff1o  24889  dvdsppwf1o  24893  dvdsflf1o  24894  fsumdvdsmul  24902  sgmmul  24907  fsumvma  24919  bposlem6  24995  lgsdchr  25061  rpvmasum2  25182  pntpbnd1  25256  ostthlem1  25297  tgbtwntriv2  25363  ercgrg  25393  hlpasch  25629  colhp  25643  colinearalglem4  25770  axlowdimlem15  25817  axcontlem7  25831  axcontlem8  25832  axcontlem10  25834  usgr1v  26129  pthdivtx  26606  grpolcan  27354  nvmf  27470  sspmval  27558  nmosetre  27589  sspph  27680  minvecolem7  27709  hiassdi  27918  shscli  28146  fh1  28447  fh2  28448  cm2j  28449  chscllem2  28467  spansncvi  28481  5oalem2  28484  adjsym  28662  nmopsetretALT  28692  nmfnsetre  28706  cnvadj  28721  cnvunop  28747  unoplin  28749  hmoplin  28771  lnopmi  28829  hmops  28849  hmopm  28850  nmcexi  28855  adjlnop  28915  adjmul  28921  adjadd  28922  opsqrlem1  28969  mdsl0  29139  ssmd2  29141  mdexchi  29164  superpos  29183  chrelat2i  29194  atcvatlem  29214  atcvati  29215  chirredlem1  29219  chirredi  29223  atcvat3i  29225  atcvat4i  29226  mdsymlem3  29234  mdsymlem5  29236  cdj3lem2b  29266  isoun  29453  xrge0infss  29499  ddemeas  30273  fsum2dsub  30659  hgt750lemb  30708  bnj1145  31035  subfacp1lem3  31138  subfacp1lem5  31140  frind  31714  sltres  31789  nodenselem5  31812  nodenselem6  31813  nodense  31816  btwnconn1lem12  32180  colinbtwnle  32200  broutsideof2  32204  lineelsb2  32230  nn0prpwlem  32292  neibastop2lem  32330  tailfb  32347  onsuct0  32415  finxpreclem2  33198  lindsenlbs  33375  poimirlem4  33384  poimirlem26  33406  poimirlem27  33407  poimirlem31  33411  heicant  33415  mblfinlem2  33418  mblfinlem3  33419  ismblfin  33421  ftc1anclem5  33460  ftc1anclem6  33461  ftc1anc  33464  sdclem1  33510  seqpo  33514  sstotbnd  33545  cntotbnd  33566  ismtycnv  33572  ismtyres  33578  heibor  33591  exidreslem  33647  ghomdiv  33662  grpokerinj  33663  rngohomco  33744  rngoisoco  33752  idlsubcl  33793  divrngidl  33798  ispridl2  33808  ispridlc  33840  riotasv3d  34065  omllaw3  34351  omlfh1N  34364  hlrelat2  34508  cvratlem  34526  cvrat  34527  cvrat3  34547  cvrat4  34548  ps-2  34583  elpaddn0  34905  paddss12  34924  pmodlem2  34952  cdleme0cq  35321  cdlemeg49lebilem  35646  cdleme50eq  35648  tendoeq2  35881  tendoex  36082  diameetN  36164  diainN  36165  dvhopN  36224  djajN  36245  dihmeetcl  36453  mapdheq2  36837  fphpdo  37200  pell1234qrne0  37236  pell14qrgt0  37242  pell1qrge1  37253  monotoddzzfi  37326  expmordi  37331  jm2.18  37374  wepwsolem  37431  dnnumch3  37436  dnwech  37437  kelac1  37452  kercvrlsm  37472  dssmapnvod  38134  gsumws3  38319  gsumws4  38320  cncmpmax  39011  fiiuncl  39054  choicefi  39208  fvelima2  39291  mullimc  39648  mullimcf  39655  idlimc  39658  limclner  39683  climleltrp  39708  limsupub  39736  climuzlem  39775  climliminflimsup2  39835  fperdvper  39896  ioodvbdlimc1lem2  39910  ioodvbdlimc2lem  39912  dvnprodlem1  39924  stoweidlem27  40007  stoweidlem48  40028  fourierdlem42  40129  fourierdlem63  40149  fourierdlem65  40151  dfsalgen2  40322  subsaliuncl  40339  sge0iunmptlemfi  40393  sge0rpcpnf  40401  iundjiun  40440  psmeasure  40451  ovnsubaddlem2  40548  hoidmvle  40577  ovolval4lem2  40627  ovolval5lem3  40631  smflimlem2  40743  smflimlem3  40744  smflimlem6  40747  smflimmpt  40779  icceuelpart  41136  mgmhmpropd  41550  subsubmgm  41562  srhmsubc  41841  srhmsubcALTV  41859
  Copyright terms: Public domain W3C validator