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 488 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 595 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  ad2ant2l  745  ad2ant2rl  748  cases2ALT  1044  consensus  1048  3ad2antr2  1186  3ad2antr3  1187  po2ne  5457  opabssxpd  5757  wfi  6153  ordelord  6185  foco  6581  f1cofveqaeqALT  6999  isocnv  7066  isores2  7069  f1oiso2  7088  offval  7400  ordsucun  7524  xp2nd  7708  2ndconst  7783  wfrdmcl  7950  smoord  7989  tfrlem9  8008  tfrlem11  8011  oaass  8174  omordi  8179  omwordri  8185  odi  8192  oewordri  8205  nnawordi  8234  nnmordi  8244  dom2lem  8536  fundmen  8570  sbthlem9  8623  mapen  8669  mapunen  8674  ssenen  8679  domfi  8727  mapfien  8859  inf3lem6  9084  r1val1  9203  rankval3b  9243  numacn  9464  infxpabs  9627  infxp  9630  cfsmolem  9685  infpssrlem4  9721  fin23lem27  9743  isf34lem4  9792  hsmexlem2  9842  axdc3lem2  9866  axdc3lem4  9868  iundom2g  9955  gchen1  10040  fpwwe2lem7  10051  fpwwe2lem11  10055  fpwwe2lem12  10056  prlem936  10462  muladd  11065  leord1  11160  eqord1  11161  ltord2  11162  leord2  11163  eqord2  11164  divadddiv  11348  ltmul12a  11489  lemul12b  11490  fimaxre  11577  supadd  11600  supmullem1  11602  cju  11625  zextlt  12048  zmax  12337  xrre  12554  supxr  12698  ixxdisj  12745  iooshf  12808  icodisj  12858  ioojoin  12865  iccshftr  12868  iccshftl  12870  iccdil  12872  icccntr  12874  iccf1o  12878  fzaddel  12940  fzsubel  12942  modadd1  13275  modmul1  13291  seqcaopr  13407  expsub  13477  expmordi  13531  sqlecan  13571  facndiv  13648  hashss  13770  hashfacen  13812  hashf1lem1  13813  fi1uzind  13855  brfi1indALT  13858  ccatpfx  14058  swrdccatfn  14081  swrdccatin2  14086  2cshwcshw  14182  resqrex  14606  fprodeq0  15325  lcmdvds  15946  hashdvds  16106  eulerthlem2  16113  pceu  16177  pcqcl  16187  infpnlem1  16240  4sqlem11  16285  ramcl  16359  prmgaplem5  16385  imasvscafn  16806  invfun  17030  initoeu2lem2  17271  catcisolem  17362  funcestrcsetclem8  17393  fullestrcsetc  17397  embedsetcestrclem  17403  funcsetcestrclem8  17408  fullsetcestrc  17412  prfcl  17449  prf1st  17450  prf2nd  17451  1st2ndprf  17452  curfuncf  17484  ipodrsfi  17769  mhmpropd  17958  subsubm  17977  pwsdiagmhm  17991  gsumccatOLD  18001  frmdgsum  18023  grplcan  18157  grplmulf1o  18169  dfgrp3lem  18193  mulgsubcl  18238  subsubg  18298  eqger  18326  resghm  18370  conjghm  18385  orbsta  18439  psgnunilem2  18619  odmulg  18679  sylow2a  18740  sylow3lem1  18748  lsmssv  18764  pj1ghm  18825  frgpup1  18897  ghmplusg  18963  subsubrg  19558  issrngd  19629  lmhmco  19812  lmhmf1o  19815  lmhmima  19816  lmhmpreima  19817  reslmhm  19821  pwsdiaglmhm  19826  pwssplit2  19829  pwssplit3  19830  pj1lmhm  19869  lspdisj  19894  prmirred  20192  cygznlem3  20265  frlmsslsp  20489  frlmlbs  20490  frlmup1  20491  issubassa2  20582  psrbagconf1o  20616  evlslem2  20755  evlslem1  20758  ply1sclf1  20922  mamuass  21011  dmatmul  21106  dmatsubcl  21107  dmatmulcl  21109  dmatcrng  21111  scmatcrng  21130  mdetunilem9  21229  pm2mpghm  21425  fvmptnn04ifb  21460  toponmre  21702  neiptopreu  21742  ordtbas  21801  txcls  22213  txlm  22257  qtoptop2  22308  qtoprest  22326  kqt0lem  22345  ptuncnv  22416  fmfnfmlem4  22566  alexsubALTlem2  22657  tgpmulg  22702  blin  23032  xmeter  23044  xmetresbl  23048  dscmet  23183  nmdvr  23280  metnrmlem3  23470  icccvx  23559  bndth  23567  htpycc  23589  pcohtpylem  23628  pi1blem  23648  lmmbrf  23870  iscfil2  23874  iscau4  23887  minveclem7  24043  elovolm  24083  dyaddisjlem  24203  ismbfd  24247  itg1mulc  24312  dvlip  24600  dvcvx  24627  plypf1  24813  eff1olem  25144  logccv  25258  lawcos  25406  leibpilem1  25530  sqff1o  25771  dvdsppwf1o  25775  dvdsflf1o  25776  fsumdvdsmul  25784  sgmmul  25789  fsumvma  25801  bposlem6  25877  lgsdchr  25943  rpvmasum2  26100  pntpbnd1  26174  ostthlem1  26215  tgbtwntriv2  26285  ercgrg  26315  hlpasch  26554  colinearalglem4  26707  axlowdimlem15  26754  axcontlem7  26768  axcontlem8  26769  axcontlem10  26771  usgr1v  27050  pthdivtx  27522  clwwlkn1loopb  27832  grpolcan  28317  nvmf  28432  sspmval  28520  nmosetre  28551  minvecolem7  28670  hiassdi  28878  shscli  29104  fh1  29405  fh2  29406  cm2j  29407  chscllem2  29425  spansncvi  29439  5oalem2  29442  adjsym  29620  nmopsetretALT  29650  nmfnsetre  29664  cnvadj  29679  cnvunop  29705  unoplin  29707  hmoplin  29729  lnopmi  29787  hmops  29807  hmopm  29808  nmcexi  29813  adjlnop  29873  adjmul  29879  adjadd  29880  opsqrlem1  29927  mdsl0  30097  ssmd2  30099  mdexchi  30122  superpos  30141  chrelat2i  30152  atcvatlem  30172  atcvati  30173  chirredlem1  30177  chirredi  30181  atcvat3i  30183  atcvat4i  30184  mdsymlem3  30192  mdsymlem5  30194  cdj3lem2b  30224  isoun  30465  xrge0infss  30514  extdg1id  31145  ddemeas  31609  fsum2dsub  31992  hgt750lemb  32041  bnj1145  32379  subfacp1lem3  32543  subfacp1lem5  32545  satfv1lem  32723  frpoind  33194  frind  33199  sltres  33283  nodenselem5  33306  nodenselem6  33307  nodense  33310  btwnconn1lem12  33673  colinbtwnle  33693  broutsideof2  33697  lineelsb2  33723  nn0prpwlem  33784  neibastop2lem  33822  tailfb  33839  onsuct0  33903  finxpreclem2  34808  lindsenlbs  35051  poimirlem4  35060  poimirlem26  35082  poimirlem27  35083  poimirlem31  35087  heicant  35091  mblfinlem2  35094  mblfinlem3  35095  ismblfin  35097  ftc1anclem5  35133  ftc1anclem6  35134  ftc1anc  35137  sdclem1  35180  seqpo  35184  sstotbnd  35212  cntotbnd  35233  ismtycnv  35239  ismtyres  35245  heibor  35258  exidreslem  35314  ghomdiv  35329  grpokerinj  35330  rngohomco  35411  rngoisoco  35419  idlsubcl  35460  divrngidl  35465  ispridl2  35475  ispridlc  35507  riotasv3d  36255  omllaw3  36540  omlfh1N  36553  hlrelat2  36698  cvratlem  36716  cvrat  36717  cvrat3  36737  cvrat4  36738  ps-2  36773  elpaddn0  37095  paddss12  37114  pmodlem2  37142  cdleme0cq  37510  cdlemeg49lebilem  37834  cdleme50eq  37836  tendoeq2  38069  tendoex  38270  diameetN  38351  diainN  38352  dvhopN  38411  djajN  38432  dihmeetcl  38640  mapdheq2  39024  3factsumint1  39308  metakunt16  39362  fsuppind  39453  0prjspn  39611  fphpdo  39755  pell1234qrne0  39791  pell14qrgt0  39797  pell1qrge1  39808  monotoddzzfi  39880  jm2.18  39926  wepwsolem  39983  dnnumch3  39988  dnwech  39989  kelac1  40004  kercvrlsm  40024  dssmapnvod  40718  gsumws3  40899  gsumws4  40900  mnuprdlem1  40977  mnuprdlem2  40978  cncmpmax  41658  fiiuncl  41696  choicefi  41826  fvelima2  41895  mullimc  42255  mullimcf  42262  idlimc  42265  limclner  42290  climleltrp  42315  limsupub  42343  climuzlem  42382  climliminflimsup2  42448  xlimbr  42466  xlimxrre  42470  dfxlim2v  42486  fperdvper  42558  ioodvbdlimc1lem2  42571  ioodvbdlimc2lem  42573  dvnprodlem1  42585  stoweidlem27  42666  stoweidlem48  42687  fourierdlem42  42788  fourierdlem63  42808  fourierdlem65  42810  dfsalgen2  42978  subsaliuncl  42995  sge0iunmptlemfi  43049  sge0rpcpnf  43057  iundjiun  43096  psmeasure  43107  ovnsubaddlem2  43207  hoidmvle  43236  ovolval4lem2  43286  ovolval5lem3  43290  smflimlem2  43402  smflimlem3  43403  smflimlem6  43406  smflimmpt  43438  icceuelpart  43950  mgmhmpropd  44402  subsubmgm  44414  srhmsubc  44697  srhmsubcALTV  44715
  Copyright terms: Public domain W3C validator