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

Theorem adantrl 752
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 476 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 490 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  797  ad2ant2rl  800  cases2ALT  1017  consensus  1023  3ad2antr2  1247  3ad2antr3  1248  opabssxpd  5370  wfi  5751  ordelord  5783  foco  6163  f1cofveqaeqALT  6556  isocnv  6620  isores2  6623  f1oiso2  6642  offval  6946  ordsucun  7067  xp2nd  7243  1stconst  7310  2ndconst  7311  wfrdmcl  7468  smoord  7507  tfrlem9  7526  tfrlem11  7529  oaass  7686  omordi  7691  omwordri  7697  odi  7704  oewordri  7717  nnawordi  7746  nnmordi  7756  dom2lem  8037  fundmen  8071  sbthlem9  8119  mapen  8165  mapunen  8170  ssenen  8175  domfi  8222  mapfien  8354  inf3lem6  8568  r1val1  8687  rankval3b  8727  numacn  8910  infxpabs  9072  infxp  9075  cfsmolem  9130  infpssrlem4  9166  fin23lem27  9188  isf34lem4  9237  hsmexlem2  9287  axdc3lem2  9311  axdc3lem4  9313  iundom2g  9400  gchen1  9485  fpwwe2lem7  9496  fpwwe2lem11  9500  fpwwe2lem12  9501  prlem936  9907  muladd  10500  leord1  10593  eqord1  10594  ltord2  10595  leord2  10596  eqord2  10597  divadddiv  10778  ltmul12a  10917  lemul12b  10918  supadd  11029  supmullem1  11031  cju  11054  zextlt  11489  zmax  11823  xrre  12038  supxr  12181  ixxdisj  12228  iooshf  12290  icodisj  12335  ioojoin  12341  iccshftr  12344  iccshftl  12346  iccdil  12348  icccntr  12350  iccf1o  12354  fzaddel  12413  fzsubel  12415  modadd1  12747  modmul1  12763  seqcaopr  12878  expsub  12948  sqlecan  13011  facndiv  13115  hashss  13235  hashfacen  13276  hashf1lem1  13277  fi1uzind  13317  brfi1indALT  13320  swrdccatin12lem2b  13532  2cshwcshw  13617  resqrex  14035  fprodeq0  14749  lcmdvds  15368  hashdvds  15527  eulerthlem2  15534  pceu  15598  pcqcl  15608  infpnlem1  15661  4sqlem11  15706  ramcl  15780  prmgaplem5  15806  imasvscafn  16244  invfun  16471  initoeu2lem2  16712  catcisolem  16803  funcestrcsetclem8  16834  fullestrcsetc  16838  embedsetcestrclem  16844  funcsetcestrclem8  16849  fullsetcestrc  16853  prfcl  16890  prf1st  16891  prf2nd  16892  1st2ndprf  16893  curfuncf  16925  ipodrsfi  17210  mhmpropd  17388  subsubm  17404  pwsdiagmhm  17416  gsumccat  17425  frmdgsum  17446  grplcan  17524  grplmulf1o  17536  dfgrp3lem  17560  mulgsubcl  17602  subsubg  17664  eqger  17691  resghm  17723  conjghm  17738  orbsta  17792  psgnunilem2  17961  odmulg  18019  sylow2a  18080  sylow3lem1  18088  lsmssv  18104  pj1ghm  18162  frgpup1  18234  ghmplusg  18295  subsubrg  18854  issrngd  18909  lmhmco  19091  lmhmf1o  19094  lmhmima  19095  lmhmpreima  19096  reslmhm  19100  pwsdiaglmhm  19105  pwssplit2  19108  pwssplit3  19109  pj1lmhm  19148  lspdisj  19173  issubassa2  19393  psrbagconf1o  19422  evlslem2  19560  evlslem1  19563  ply1sclf1  19707  prmirred  19891  cygznlem3  19966  frlmsslsp  20183  frlmlbs  20184  frlmup1  20185  mamuass  20256  dmatmul  20351  dmatsubcl  20352  dmatmulcl  20354  dmatcrng  20356  scmatcrng  20375  mdetunilem9  20474  pm2mpghm  20669  fvmptnn04ifb  20704  toponmre  20945  neiptopreu  20985  ordtbas  21044  txcls  21455  txlm  21499  qtoptop2  21550  qtoprest  21568  kqt0lem  21587  ptuncnv  21658  fmfnfmlem4  21808  alexsubALTlem2  21899  tgpmulg  21944  blin  22273  xmeter  22285  xmetresbl  22289  dscmet  22424  nmdvr  22521  metnrmlem3  22711  icccvx  22796  bndth  22804  htpycc  22826  pcohtpylem  22865  pi1blem  22885  lmmbrf  23106  iscfil2  23110  iscau4  23123  minveclem7  23252  elovolm  23289  dyaddisjlem  23409  ismbfd  23452  itg1mulc  23516  dvlip  23801  dvcvx  23828  plypf1  24013  eff1olem  24339  logccv  24454  lawcos  24591  sqff1o  24953  dvdsppwf1o  24957  dvdsflf1o  24958  fsumdvdsmul  24966  sgmmul  24971  fsumvma  24983  bposlem6  25059  lgsdchr  25125  rpvmasum2  25246  pntpbnd1  25320  ostthlem1  25361  tgbtwntriv2  25427  ercgrg  25457  hlpasch  25693  colhp  25707  colinearalglem4  25834  axlowdimlem15  25881  axcontlem7  25895  axcontlem8  25896  axcontlem10  25898  usgr1v  26193  pthdivtx  26681  clwwlkn1loopb  27006  grpolcan  27512  nvmf  27628  sspmval  27716  nmosetre  27747  sspph  27838  minvecolem7  27867  hiassdi  28076  shscli  28304  fh1  28605  fh2  28606  cm2j  28607  chscllem2  28625  spansncvi  28639  5oalem2  28642  adjsym  28820  nmopsetretALT  28850  nmfnsetre  28864  cnvadj  28879  cnvunop  28905  unoplin  28907  hmoplin  28929  lnopmi  28987  hmops  29007  hmopm  29008  nmcexi  29013  adjlnop  29073  adjmul  29079  adjadd  29080  opsqrlem1  29127  mdsl0  29297  ssmd2  29299  mdexchi  29322  superpos  29341  chrelat2i  29352  atcvatlem  29372  atcvati  29373  chirredlem1  29377  chirredi  29381  atcvat3i  29383  atcvat4i  29384  mdsymlem3  29392  mdsymlem5  29394  cdj3lem2b  29424  isoun  29607  xrge0infss  29653  ddemeas  30427  fsum2dsub  30813  hgt750lemb  30862  bnj1145  31187  subfacp1lem3  31290  subfacp1lem5  31292  frpoind  31865  frind  31868  sltres  31940  nodenselem5  31963  nodenselem6  31964  nodense  31967  btwnconn1lem12  32330  colinbtwnle  32350  broutsideof2  32354  lineelsb2  32380  nn0prpwlem  32442  neibastop2lem  32480  tailfb  32497  onsuct0  32565  finxpreclem2  33357  lindsenlbs  33534  poimirlem4  33543  poimirlem26  33565  poimirlem27  33566  poimirlem31  33570  heicant  33574  mblfinlem2  33577  mblfinlem3  33578  ismblfin  33580  ftc1anclem5  33619  ftc1anclem6  33620  ftc1anc  33623  sdclem1  33669  seqpo  33673  sstotbnd  33704  cntotbnd  33725  ismtycnv  33731  ismtyres  33737  heibor  33750  exidreslem  33806  ghomdiv  33821  grpokerinj  33822  rngohomco  33903  rngoisoco  33911  idlsubcl  33952  divrngidl  33957  ispridl2  33967  ispridlc  33999  riotasv3d  34564  omllaw3  34850  omlfh1N  34863  hlrelat2  35007  cvratlem  35025  cvrat  35026  cvrat3  35046  cvrat4  35047  ps-2  35082  elpaddn0  35404  paddss12  35423  pmodlem2  35451  cdleme0cq  35820  cdlemeg49lebilem  36144  cdleme50eq  36146  tendoeq2  36379  tendoex  36580  diameetN  36662  diainN  36663  dvhopN  36722  djajN  36743  dihmeetcl  36951  mapdheq2  37335  fphpdo  37698  pell1234qrne0  37734  pell14qrgt0  37740  pell1qrge1  37751  monotoddzzfi  37824  expmordi  37829  jm2.18  37872  wepwsolem  37929  dnnumch3  37934  dnwech  37935  kelac1  37950  kercvrlsm  37970  dssmapnvod  38631  gsumws3  38816  gsumws4  38817  cncmpmax  39505  fiiuncl  39548  choicefi  39706  fvelima2  39789  mullimc  40166  mullimcf  40173  idlimc  40176  limclner  40201  climleltrp  40226  limsupub  40254  climuzlem  40293  climliminflimsup2  40359  xlimbr  40371  xlimxrre  40375  dfxlim2v  40391  fperdvper  40451  ioodvbdlimc1lem2  40465  ioodvbdlimc2lem  40467  dvnprodlem1  40479  stoweidlem27  40562  stoweidlem48  40583  fourierdlem42  40684  fourierdlem63  40704  fourierdlem65  40706  dfsalgen2  40877  subsaliuncl  40894  sge0iunmptlemfi  40948  sge0rpcpnf  40956  iundjiun  40995  psmeasure  41006  ovnsubaddlem2  41106  hoidmvle  41135  ovolval4lem2  41185  ovolval5lem3  41189  smflimlem2  41301  smflimlem3  41302  smflimlem6  41305  smflimmpt  41337  icceuelpart  41697  mgmhmpropd  42110  subsubmgm  42122  srhmsubc  42401  srhmsubcALTV  42419
  Copyright terms: Public domain W3C validator