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

Theorem adantrl 747
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 475 . 2 ((𝜃𝜓) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 489 1 ((𝜑 ∧ (𝜃𝜓)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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 195  df-an 384
This theorem is referenced by:  ad2ant2l  777  ad2ant2rl  780  consensus  989  cases2  1004  3ad2antr2  1219  3ad2antr3  1220  wfi  5615  ordelord  5647  foco  6022  isocnv  6457  isores2  6460  f1oiso2  6479  offval  6779  ordsucun  6894  opabex2  6974  xp2nd  7067  1stconst  7129  2ndconst  7130  wfrdmcl  7287  smoord  7326  tfrlem9  7345  tfrlem11  7348  oaass  7505  omordi  7510  omwordri  7516  odi  7523  oewordri  7536  nnawordi  7565  nnmordi  7575  dom2lem  7858  fundmen  7893  sbthlem9  7940  mapen  7986  mapunen  7991  ssenen  7996  domfi  8043  mapfien  8173  inf3lem6  8390  r1val1  8509  rankval3b  8549  numacn  8732  infxpabs  8894  infxp  8897  cfsmolem  8952  infpssrlem4  8988  fin23lem27  9010  isf34lem4  9059  hsmexlem2  9109  axdc3lem2  9133  axdc3lem4  9135  iundom2g  9218  gchen1  9303  fpwwe2lem7  9314  fpwwe2lem11  9318  fpwwe2lem12  9319  prlem936  9725  muladd  10313  leord1  10406  eqord1  10407  ltord2  10408  leord2  10409  eqord2  10410  divadddiv  10591  ltmul12a  10730  lemul12b  10731  supadd  10840  supmullem1  10842  cju  10865  zextlt  11285  zmax  11619  xrre  11835  supxr  11973  ixxdisj  12019  iooshf  12081  icodisj  12126  ioojoin  12132  iccshftr  12135  iccshftl  12137  iccdil  12139  icccntr  12141  iccf1o  12145  fzaddel  12203  fzsubel  12205  modadd1  12526  modmul1  12542  seqcaopr  12657  expsub  12727  sqlecan  12790  facndiv  12894  hashss  13012  hashfacen  13049  hashf1lem1  13050  fi1uzind  13082  brfi1indALT  13085  fi1uzindOLD  13088  brfi1indALTOLD  13091  swrdccatin12lem2b  13285  2cshwcshw  13370  resqrex  13787  fprodeq0  14492  lcmdvds  15107  hashdvds  15266  eulerthlem2  15273  pceu  15337  pcqcl  15347  infpnlem1  15400  4sqlem11  15445  ramcl  15519  prmgaplem5  15545  imasvscafn  15968  invfun  16195  initoeu2lem2  16436  catcisolem  16527  funcestrcsetclem8  16558  fullestrcsetc  16562  embedsetcestrclem  16568  funcsetcestrclem8  16573  fullsetcestrc  16577  prfcl  16614  prf1st  16615  prf2nd  16616  1st2ndprf  16617  curfuncf  16649  ipodrsfi  16934  mhmpropd  17112  subsubm  17128  pwsdiagmhm  17140  gsumccat  17149  frmdgsum  17170  grplcan  17248  grplmulf1o  17260  dfgrp3lem  17284  mulgsubcl  17326  subsubg  17388  eqger  17415  resghm  17447  conjghm  17462  orbsta  17517  psgnunilem2  17686  odmulg  17744  sylow2a  17805  sylow3lem1  17813  lsmssv  17829  pj1ghm  17887  frgpup1  17959  ghmplusg  18020  subsubrg  18577  issrngd  18632  lmhmco  18812  lmhmf1o  18815  lmhmima  18816  lmhmpreima  18817  reslmhm  18821  pwsdiaglmhm  18826  pwssplit2  18829  pwssplit3  18830  pj1lmhm  18869  lspdisj  18894  issubassa2  19114  psrbagconf1o  19143  evlslem2  19281  evlslem1  19284  ply1sclf1  19428  prmirred  19609  cygznlem3  19684  frlmsslsp  19901  frlmlbs  19902  frlmup1  19903  mamuass  19974  dmatmul  20069  dmatsubcl  20070  dmatmulcl  20072  dmatcrng  20074  scmatcrng  20093  mdetunilem9  20192  pm2mpghm  20387  fvmptnn04ifb  20422  toponmre  20654  neiptopreu  20694  ordtbas  20753  txcls  21164  txlm  21208  qtoptop2  21259  qtoprest  21277  kqt0lem  21296  ptuncnv  21367  fmfnfmlem4  21518  alexsubALTlem2  21609  tgpmulg  21654  blin  21983  xmeter  21995  xmetresbl  21999  dscmet  22134  nmdvr  22231  metnrmlem3  22419  icccvx  22504  bndth  22512  htpycc  22534  pcohtpylem  22574  pi1blem  22594  lmmbrf  22812  iscfil2  22816  iscau4  22829  minveclem7  22958  elovolm  22994  dyaddisjlem  23113  ismbfd  23157  itg1mulc  23221  dvlip  23504  dvcvx  23531  plypf1  23716  eff1olem  24042  logccv  24153  lawcos  24290  sqff1o  24652  dvdsppwf1o  24656  dvdsflf1o  24657  fsumdvdsmul  24665  sgmmul  24670  fsumvma  24682  bposlem6  24758  lgsdchr  24824  rpvmasum2  24945  pntpbnd1  25019  ostthlem1  25060  tgbtwntriv2  25126  ercgrg  25157  hlpasch  25393  colhp  25407  colinearalglem4  25534  axlowdimlem15  25581  axcontlem7  25595  axcontlem8  25596  axcontlem10  25598  spthonepeq  25910  usgra2adedgspth  25934  usgra2adedgwlk  25935  usgra2adedgwlkon  25936  numclwlk1lem2f1  26414  grpolcan  26561  nvmf  26677  sspmval  26765  nmosetre  26796  sspph  26887  minvecolem7  26916  hiassdi  27125  shscli  27353  fh1  27654  fh2  27655  cm2j  27656  chscllem2  27674  spansncvi  27688  5oalem2  27691  adjsym  27869  nmopsetretALT  27899  nmfnsetre  27913  cnvadj  27928  cnvunop  27954  unoplin  27956  hmoplin  27978  lnopmi  28036  hmops  28056  hmopm  28057  nmcexi  28062  adjlnop  28122  adjmul  28128  adjadd  28129  opsqrlem1  28176  mdsl0  28346  ssmd2  28348  mdexchi  28371  superpos  28390  chrelat2i  28401  atcvatlem  28421  atcvati  28422  chirredlem1  28426  chirredi  28430  atcvat3i  28432  atcvat4i  28433  mdsymlem3  28441  mdsymlem5  28443  cdj3lem2b  28473  isoun  28655  xrge0infss  28708  ddemeas  29419  bnj1145  30108  subfacp1lem3  30211  subfacp1lem5  30213  frind  30777  sltres  30854  nodenselem6  30878  nodenselem7  30879  nodense  30881  nofulllem5  30898  btwnconn1lem12  31168  colinbtwnle  31188  broutsideof2  31192  lineelsb2  31218  nn0prpwlem  31280  neibastop2lem  31318  tailfb  31335  onsuct0  31403  finxpreclem2  32186  lindsenlbs  32357  poimirlem4  32366  poimirlem26  32388  poimirlem27  32389  poimirlem31  32393  heicant  32397  mblfinlem2  32400  mblfinlem3  32401  ismblfin  32403  ftc1anclem5  32442  ftc1anclem6  32443  ftc1anc  32446  sdclem1  32492  seqpo  32496  sstotbnd  32527  cntotbnd  32548  ismtycnv  32554  ismtyres  32560  heibor  32573  exidreslem  32629  ghomdiv  32644  grpokerinj  32645  rngohomco  32726  rngoisoco  32734  idlsubcl  32775  divrngidl  32780  ispridl2  32790  ispridlc  32822  riotasv3d  33047  omllaw3  33333  omlfh1N  33346  hlrelat2  33490  cvratlem  33508  cvrat  33509  cvrat3  33529  cvrat4  33530  ps-2  33565  elpaddn0  33887  paddss12  33906  pmodlem2  33934  cdleme0cq  34303  cdlemeg49lebilem  34628  cdleme50eq  34630  tendoeq2  34863  tendoex  35064  diameetN  35146  diainN  35147  dvhopN  35206  djajN  35227  dihmeetcl  35435  mapdheq2  35819  fphpdo  36182  pell1234qrne0  36218  pell14qrgt0  36224  pell1qrge1  36235  monotoddzzfi  36308  expmordi  36313  jm2.18  36356  wepwsolem  36413  dnnumch3  36418  dnwech  36419  kelac1  36434  kercvrlsm  36454  dssmapnvod  37117  gsumws3  37304  gsumws4  37305  cncmpmax  37997  fiiuncl  38042  choicefi  38170  mullimc  38466  mullimcf  38473  idlimc  38476  limclner  38501  climleltrp  38526  fperdvper  38591  ioodvbdlimc1lem2  38605  ioodvbdlimc2lem  38607  dvnprodlem1  38619  stoweidlem27  38703  stoweidlem48  38724  fourierdlem42  38825  fourierdlem63  38845  fourierdlem65  38847  dfsalgen2  39018  subsaliuncl  39035  sge0iunmptlemfi  39089  sge0rpcpnf  39097  iundjiun  39136  psmeasure  39147  ovnsubaddlem2  39244  hoidmvle  39273  ovolval4lem2  39323  ovolval5lem3  39327  smflimlem2  39441  smflimlem3  39442  smflimlem6  39445  icceuelpart  39758  f1cofveqaeqALT  40119  usgr1v  40463  pthdivtx  40916  mgmhmpropd  41556  subsubmgm  41568  srhmsubc  41849  srhmsubcALTV  41868
  Copyright terms: Public domain W3C validator