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

Theorem adantrl 714
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 485 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 593 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396
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 397
This theorem is referenced by:  ad2ant2l  744  ad2ant2rl  747  cases2ALT  1047  consensus  1051  3ad2antr2  1189  3ad2antr3  1190  po2ne  5561  opabssxpd  5679  frpoind  6296  wfiOLD  6305  ordelord  6339  f1un  6804  f1cofveqaeqALT  7205  isocnv  7274  isores2  7277  f1oiso2  7296  offval  7625  ordsucun  7759  xp2nd  7953  2ndconst  8032  sexp2  8077  wfrdmclOLD  8262  smoord  8310  tfrlem9  8330  tfrlem11  8333  oaass  8507  omordi  8512  omwordri  8518  odi  8525  oewordri  8538  nnawordi  8567  nnmordi  8577  coflton  8616  dom2lem  8931  fundmen  8974  sbthlem9  9034  mapen  9084  mapunen  9089  ssenen  9094  domfi  9135  mapfien  9343  inf3lem6  9568  ttrclselem2  9661  frind  9685  r1val1  9721  rankval3b  9761  numacn  9984  infxpabs  10147  infxp  10150  cfsmolem  10205  infpssrlem4  10241  fin23lem27  10263  isf34lem4  10312  hsmexlem2  10362  axdc3lem2  10386  axdc3lem4  10388  iundom2g  10475  gchen1  10560  fpwwe2lem6  10571  fpwwe2lem10  10575  fpwwe2lem11  10576  prlem936  10982  muladd  11586  leord1  11681  eqord1  11682  ltord2  11683  leord2  11684  eqord2  11685  divadddiv  11869  ltmul12a  12010  lemul12b  12011  fimaxre  12098  supadd  12122  supmullem1  12124  cju  12148  zextlt  12576  zmax  12869  xrre  13087  supxr  13231  ixxdisj  13278  iooshf  13342  icodisj  13392  ioojoin  13399  iccshftr  13402  iccshftl  13404  iccdil  13406  icccntr  13408  iccf1o  13412  fzaddel  13474  fzsubel  13476  modadd1  13812  modmul1  13828  seqcaopr  13944  expsub  14015  expmordi  14071  sqlecan  14112  facndiv  14187  hashss  14308  hashfacen  14350  hashfacenOLD  14351  hashf1lem1  14352  hashf1lem1OLD  14353  fi1uzind  14395  brfi1indALT  14398  ccatpfx  14588  swrdccatfn  14611  swrdccatin2  14616  2cshwcshw  14713  resqrex  15134  fprodeq0  15857  lcmdvds  16483  hashdvds  16646  eulerthlem2  16653  pceu  16717  pcqcl  16727  infpnlem1  16781  4sqlem11  16826  ramcl  16900  prmgaplem5  16926  imasvscafn  17418  invfun  17646  initoeu2lem2  17900  catcisolem  17995  funcestrcsetclem8  18034  fullestrcsetc  18038  embedsetcestrclem  18044  funcsetcestrclem8  18049  fullsetcestrc  18053  prfcl  18090  prf1st  18091  prf2nd  18092  1st2ndprf  18093  curfuncf  18126  ipodrsfi  18427  mhmpropd  18607  subsubm  18626  pwsdiagmhm  18640  frmdgsum  18671  grplcan  18807  grplmulf1o  18819  dfgrp3lem  18843  mulgsubcl  18888  subsubg  18949  eqger  18978  resghm  19022  conjghm  19037  orbsta  19091  psgnunilem2  19275  odmulg  19336  sylow2a  19399  sylow3lem1  19407  lsmssv  19423  pj1ghm  19483  frgpup1  19555  ghmplusg  19622  subsubrg  20246  issrngd  20318  lmhmco  20502  lmhmf1o  20505  lmhmima  20506  lmhmpreima  20507  reslmhm  20511  pwsdiaglmhm  20516  pwssplit2  20519  pwssplit3  20520  pj1lmhm  20559  lspdisj  20584  prmirred  20893  cygznlem3  20974  frlmsslsp  21200  frlmlbs  21201  frlmup1  21202  issubassa2  21293  psrbagconf1o  21336  psrbagconf1oOLD  21337  psrgrp  21364  evlslem2  21487  evlslem1  21490  ply1sclf1  21658  mamuass  21747  dmatmul  21844  dmatsubcl  21845  dmatmulcl  21847  dmatcrng  21849  scmatcrng  21868  mdetunilem9  21967  pm2mpghm  22163  fvmptnn04ifb  22198  toponmre  22442  neiptopreu  22482  ordtbas  22541  txcls  22953  txlm  22997  qtoptop2  23048  qtoprest  23066  kqt0lem  23085  ptuncnv  23156  fmfnfmlem4  23306  alexsubALTlem2  23397  tgpmulg  23442  blin  23772  xmeter  23784  xmetresbl  23788  dscmet  23926  nmdvr  24032  metnrmlem3  24222  icccvx  24311  bndth  24319  htpycc  24341  pcohtpylem  24380  pi1blem  24400  lmmbrf  24624  iscfil2  24628  iscau4  24641  minveclem7  24797  elovolm  24837  dyaddisjlem  24957  ismbfd  25001  itg1mulc  25067  dvlip  25355  dvcvx  25382  plypf1  25571  eff1olem  25902  logccv  26016  lawcos  26164  leibpilem1  26288  sqff1o  26529  dvdsppwf1o  26533  dvdsflf1o  26534  fsumdvdsmul  26542  sgmmul  26547  fsumvma  26559  bposlem6  26635  lgsdchr  26701  rpvmasum2  26858  pntpbnd1  26932  ostthlem1  26973  sltres  27008  nodenselem5  27034  nodenselem6  27035  nodense  27038  addsproplem2  27280  tgbtwntriv2  27376  ercgrg  27406  hlpasch  27645  colinearalglem4  27805  axlowdimlem15  27852  axcontlem7  27866  axcontlem8  27867  axcontlem10  27869  usgr1v  28151  pthdivtx  28624  clwwlkn1loopb  28934  grpolcan  29419  nvmf  29534  sspmval  29622  nmosetre  29653  minvecolem7  29772  hiassdi  29980  shscli  30206  fh1  30507  fh2  30508  cm2j  30509  chscllem2  30527  spansncvi  30541  5oalem2  30544  adjsym  30722  nmopsetretALT  30752  nmfnsetre  30766  cnvadj  30781  cnvunop  30807  unoplin  30809  hmoplin  30831  lnopmi  30889  hmops  30909  hmopm  30910  nmcexi  30915  adjlnop  30975  adjmul  30981  adjadd  30982  opsqrlem1  31029  mdsl0  31199  ssmd2  31201  mdexchi  31224  superpos  31243  chrelat2i  31254  atcvatlem  31274  atcvati  31275  chirredlem1  31279  chirredi  31283  atcvat3i  31285  atcvat4i  31286  mdsymlem3  31294  mdsymlem5  31296  cdj3lem2b  31326  isoun  31560  xrge0infss  31609  extdg1id  32292  ddemeas  32775  fsum2dsub  33160  hgt750lemb  33209  bnj1145  33545  subfacp1lem3  33716  subfacp1lem5  33718  satfv1lem  33896  btwnconn1lem12  34673  colinbtwnle  34693  broutsideof2  34697  lineelsb2  34723  nn0prpwlem  34784  neibastop2lem  34822  tailfb  34839  onsuct0  34903  finxpreclem2  35851  lindsenlbs  36063  poimirlem4  36072  poimirlem26  36094  poimirlem27  36095  poimirlem31  36099  heicant  36103  mblfinlem2  36106  mblfinlem3  36107  ismblfin  36109  ftc1anclem5  36145  ftc1anclem6  36146  ftc1anc  36149  sdclem1  36192  seqpo  36196  sstotbnd  36224  cntotbnd  36245  ismtycnv  36251  ismtyres  36257  heibor  36270  exidreslem  36326  ghomdiv  36341  grpokerinj  36342  rngohomco  36423  rngoisoco  36431  idlsubcl  36472  divrngidl  36477  ispridl2  36487  ispridlc  36519  riotasv3d  37412  omllaw3  37697  omlfh1N  37710  hlrelat2  37856  cvratlem  37874  cvrat  37875  cvrat3  37895  cvrat4  37896  ps-2  37931  elpaddn0  38253  paddss12  38272  pmodlem2  38300  cdleme0cq  38668  cdlemeg49lebilem  38992  cdleme50eq  38994  tendoeq2  39227  tendoex  39428  diameetN  39509  diainN  39510  dvhopN  39569  djajN  39590  dihmeetcl  39798  mapdheq2  40182  3factsumint1  40468  metakunt16  40582  evlsbagval  40727  fsuppind  40742  mhphf  40748  0prjspn  40943  fphpdo  41117  pell1234qrne0  41153  pell14qrgt0  41159  pell1qrge1  41170  monotoddzzfi  41243  jm2.18  41289  wepwsolem  41346  dnnumch3  41351  dnwech  41352  kelac1  41367  kercvrlsm  41387  onov0suclim  41586  cantnfresb  41635  dssmapnvod  42273  gsumws3  42450  gsumws4  42451  mnuprdlem1  42533  mnuprdlem2  42534  cncmpmax  43218  fiiuncl  43254  choicefi  43396  fvelima2  43463  mullimc  43828  mullimcf  43835  idlimc  43838  limclner  43863  climleltrp  43888  limsupub  43916  climuzlem  43955  climliminflimsup2  44021  xlimbr  44039  xlimxrre  44043  dfxlim2v  44059  fperdvper  44131  ioodvbdlimc1lem2  44144  ioodvbdlimc2lem  44146  dvnprodlem1  44158  stoweidlem27  44239  stoweidlem48  44260  fourierdlem42  44361  fourierdlem63  44381  fourierdlem65  44383  dfsalgen2  44553  subsaliuncl  44570  sge0iunmptlemfi  44625  sge0rpcpnf  44633  iundjiun  44672  psmeasure  44683  ovnsubaddlem2  44783  hoidmvle  44812  ovolval4lem2  44862  smflimlem2  44984  smflimlem3  44985  smflimlem6  44988  smflimmpt  45022  fcoresf1  45274  icceuelpart  45599  mgmhmpropd  46050  subsubmgm  46062  srhmsubc  46345  srhmsubcALTV  46363  catprs  47002
  Copyright terms: Public domain W3C validator