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

Theorem 3adant2 1100
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Jul-1995.)
Hypothesis
Ref Expression
3adant.1 ((𝜑𝜓) → 𝜒)
Assertion
Ref Expression
3adant2 ((𝜑𝜃𝜓) → 𝜒)

Proof of Theorem 3adant2
StepHypRef Expression
1 3simpb 1079 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1054
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  df-3an 1056
This theorem is referenced by:  3ad2ant1  1102  eupickb  2567  vtoclegft  3311  eqeu  3410  funopg  5960  fnco  6037  dff1o2  6180  fnimapr  6301  fvmptt  6339  fnreseql  6367  f1elima  6560  f13dfv  6570  f1ocnvfvb  6575  oprssov  6845  ordunel  7069  poxp  7334  wfrlem4  7463  smoiso  7504  oaord  7672  oaword  7674  omcan  7694  omwordri  7697  odi  7704  omeulem1  7707  oeord  7713  oecan  7714  oewordri  7717  oeordsuc  7719  nnaord  7744  nnaordr  7745  nndi  7748  nnaword  7752  nnmwordri  7761  erov  7887  ecopovtrn  7893  xpdom3  8099  mapxpen  8167  findcard  8240  indexfi  8315  suppr  8418  infpr  8450  r111  8676  tcrank  8785  acndom  8912  infdif2  9070  infxpdom  9071  cfeq0  9116  cfsuc  9117  cfflb  9119  cflim2  9123  cfsmolem  9130  axcc3  9298  domtriomlem  9302  axdc3lem2  9311  axdc3lem4  9313  axdc4lem  9315  axcclem  9317  pwcfsdom  9443  tsktrss  9621  tsksuc  9622  tskuni  9643  adderpqlem  9814  mulerpqlem  9815  mulcanenq  9820  distrnq  9821  ltsonq  9829  ltanq  9831  ltmnq  9832  distrlem1pr  9885  distrlem5pr  9887  ltsopr  9892  ltsosr  9953  ltasr  9959  adddir  10069  axlttrn  10148  letr  10169  nnncan1  10355  npncan3  10357  pnpcan2  10359  subdi  10501  subdir  10502  mulcan1g  10718  mulcan2g  10719  divmul  10726  div23  10742  div13  10744  muldivdir  10758  divsubdir  10759  divcan7  10772  ltmul2  10912  lemul1  10913  lemul2  10914  lemul2a  10916  lediv1  10926  ltmuldiv2  10935  lemuldiv  10941  lemuldiv2  10942  ltdiv2  10947  lediv2  10951  fiminre  11010  infrelb  11046  nndivtr  11100  bndndx  11329  nn0n0n1ge2  11396  fnn0ind  11514  addlelt  11980  xrletr  12027  qsqueeze  12070  xleadd2a  12122  xleadd1  12123  xltadd2  12125  xltmul2  12161  supxrbnd  12196  iooneg  12330  iccneg  12331  icoshft  12332  icoshftf1o  12333  zltaddlt1le  12362  fzen  12396  uzsubsubfz  12401  ssfzunsnext  12424  fzrevral2  12464  fzshftral  12466  fz0fzdiffz0  12487  elfzmlbp  12489  elfzo  12511  nelfzo  12514  fzoaddel2  12563  fzosubel2  12567  elfzom1p1elfzo  12587  ssfzo12bi  12603  fzonfzoufzol  12611  subfzo0  12630  flltdivnn0lt  12674  modmulnn  12728  modcyc  12745  modaddabs  12748  modaddmod  12749  modmuladd  12752  modadd2mod  12760  modsubmod  12768  modsubmodmod  12769  modaddmodup  12773  modmulmod  12775  moddi  12778  modsubdir  12779  modfzo0difsn  12782  modsumfzodifsn  12783  uzindi  12821  axdc4uzlem  12822  expneg2  12909  expdiv  12951  expubnd  12961  mulbinom2  13024  bernneq2  13031  hashinfxadd  13212  brfi1indlem  13316  ccatval3  13397  ccatsymb  13400  ccatfv0  13401  ccatval1lsw  13402  ccats1val2  13447  swrdnd  13478  2swrd1eqwrdeq  13500  swrdswrd  13506  wrd2ind  13523  swrdccatin1  13529  swrdccatin12lem2b  13532  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12lem3  13536  swrdccat  13539  swrdccat3a  13540  swrdccat3blem  13541  repswswrd  13577  repswccat  13578  cshwidxmod  13595  2cshw  13605  3cshw  13610  scshwfzeqfzo  13618  cshwcsh2id  13620  cshimadifsn  13621  cshimadifsn0  13622  ccatco  13627  cshco  13628  swrdco  13629  lswco  13630  swrds2  13731  2swrd2eqwrdeq  13742  shftuz  13853  shftval2  13859  abs3dif  14115  fsumdifsnconst  14567  modfsummods  14569  sin02gt0  14966  dvdsval2  15030  dvdscmul  15055  dvdsmulc  15056  dvdscmulr  15057  dvdsmulcr  15058  divalglem8  15170  ndvdssub  15180  rpmulgcd  15322  coprmdvdsOLD  15414  coprmprod  15422  cncongr1  15428  cncongr2  15429  isprm3  15443  modprm0  15557  coprimeprodsq  15560  pythagtriplem12  15578  pythagtriplem14  15580  pcprendvds  15592  pcmul  15603  pcdiv  15604  pcqcl  15608  pcqdiv  15609  pcdvdsb  15620  pcgcd  15629  vdwnnlem1  15746  hashbcss  15755  cshwshashlem1  15849  fvsetsid  15937  setsstruct2  15943  setsstruct  15945  mrcss  16323  mrcsscl  16327  mrcun  16329  cofulid  16597  catcisolem  16803  funcsetcestrclem9  16850  latleeqj1  17110  lubun  17170  clatleglb  17173  pslem  17253  dirtr  17283  mgmb1mgm1  17301  pwspjmhm  17415  gsumccat  17425  grpinvid1  17517  grpinvid2  17518  grpasscan1  17525  grpasscan2  17526  grpinvadd  17540  grpsubf  17541  grpsubrcan  17543  grpinvsub  17544  grpsubeq0  17548  grpsubadd0sub  17549  grppncan  17553  grpnpcan  17554  mulgnn0p1  17599  mulgaddcomlem  17610  mulginvcom  17612  mulginvinv  17613  subgsubcl  17652  subgsub  17653  eqglact  17692  qussub  17701  ghmsub  17715  psgnunilem4  17963  oddvds2  18029  odsubdvds  18032  gexnnod  18049  slwn0  18076  gsumdixp  18655  dvrcl  18732  unitdvcl  18733  dvrcan1  18737  dvrcan3  18738  dvreq1  18739  subrgdv  18845  abvsubtri  18883  idsrngd  18910  lmodvsubval2  18966  lsmcl  19131  lsmsp2  19135  lspsntrim  19146  lidldvgen  19303  evlslem4  19556  mpfsubrg  19580  ply1tmcl  19690  eqcoe1ply1eq  19715  gsummoncoe1  19722  lply1binomsc  19725  chrcong  19925  zndvds  19946  zntoslem  19953  ocvsscon  20067  obselocv  20120  frlmphl  20168  mamudm  20242  mamufacex  20243  scmatf1  20385  scmatf1o  20386  scmatrngiso  20390  submabas  20432  mdetdiaglem  20452  mdetralt2  20463  mdetero  20464  mdetunilem2  20467  mdetunilem6  20471  m2detleiblem7  20481  maducoeval2  20494  gsummatr01lem3  20511  gsummatr01  20513  smadiadetglem2  20526  cramerlem1  20541  mply1topmatcl  20658  mp2pm2mplem4  20662  ntrin  20913  elnei  20963  neindisj2  20975  ordtopn3  21048  ordtcld3  21051  leordtval2  21064  lecldbas  21071  cnrest2  21138  cmpsublem  21250  ptrescn  21490  xkococn  21511  kqfeq  21575  snfbas  21717  neifil  21731  fclsrest  21875  utopsnnei  22100  neipcfilu  22147  psmetsym  22162  psmetge0  22164  xmetge0  22196  xmetsym  22199  metustto  22405  metustbl  22418  restmetu  22422  nm2dif  22476  nmtri  22477  cnmet  22622  cnmpt2pc  22774  iihalf1  22777  iihalf2  22779  iocopnst  22786  clmnegsubdi2  22951  clmsub4  22952  clmvsubval2  22956  ncvspi  23002  cphsqrtcl3  23033  cph2ass  23059  cphipval2  23086  cphipval  23088  caublcls  23153  bcthlem3  23169  bcthlem4  23170  srabn  23202  rrxmet  23237  iblconst  23629  tdeglem3  23864  mdegmullem  23883  dvdsq1p  23965  coeid3  24041  aannenlem2  24129  pserdvlem2  24227  tanord1  24328  cxpef  24456  recxpcl  24466  logbchbase  24554  relogbcl  24556  relogbzcl  24557  logbleb  24566  logblt  24567  relogbcxpb  24570  lawcos  24591  pythag  24592  isosctrlem1  24593  isosctrlem2  24594  lgsmodeq  25112  lgsmulsqcoprm  25113  gausslemma2dlem1a  25135  2lgsoddprmlem2  25179  ax5seglem1  25853  axcontlem2  25890  axcontlem8  25896  upgrpredgv  26079  numedglnl  26084  issubgr2  26209  uhgrissubgr  26212  egrsubgr  26214  fusgrfisstep  26266  nbusgrfi  26320  nb3grprlem2  26327  cplgr3v  26387  cusgrsizeindslem  26403  finsumvtxdg2size  26502  rusgrpropadjvtx  26537  upgrwlkvtxedg  26597  usgr2trlncl  26712  uspgrn2crct  26756  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  wwlksnextproplem3  26874  umgr2adedgwlklem  26909  rusgr0edg  26940  clwwlk1loop  26956  clwlkclwwlklem2a4  26963  clwlkclwwlklem2a  26964  clwwisshclwwslemlem  26970  erclwwlktr  26979  clwwlkel  27009  erclwwlkntr  27035  clwlksfclwwlk  27049  clwwlknonwwlknonbOLD  27081  clwwlknonex2lem2  27083  uhgr3cyclex  27160  umgr3cyclex  27161  eucrctshift  27221  frgr3v  27255  3cyclfrgrrn  27266  frgrwopreglem5a  27291  frgr2wsp1  27310  numclwlk3lem3  27322  2clwwlk2clwwlklem2lem2  27329  clwwlkccatlem  27331  numclwwlk5  27375  numclwwlk6  27377  isgrpo  27479  grpoinvid1  27510  grpoinvid2  27511  grpoinvop  27515  grpodivinv  27518  grpoinvdiv  27519  grpodivf  27520  grponpcan  27525  ablonncan  27539  nvmval  27625  nvmval2  27626  nvmfval  27627  nvmul0or  27633  nvpncan2  27636  nvaddsub4  27640  nvmeq0  27641  nvdif  27649  nvpi  27650  nvmtri  27654  nvabs  27655  imsmetlem  27673  ipval2lem3  27688  ipval2  27690  4ipval2  27691  ipval3  27692  nmooge0  27750  blometi  27786  hvaddsub12  28023  hvsubdistr1  28034  hvsubdistr2  28035  hvaddcan2  28056  hvmulcan  28057  hvmulcan2  28058  hvsubcan  28059  hvsubcan2  28060  his7  28075  his2sub  28077  his2sub2  28078  norm3dif2  28136  shsubcl  28205  hhssnv  28249  shlej2  28348  fh2  28606  cm2j  28607  pjoi0  28704  hodcl  28734  hosubdi  28795  unopf1o  28903  unopadj  28906  adj2  28921  braadd  28932  bramul  28933  lnopaddmuli  28960  lnopsubmuli  28962  homco2  28964  lnfnaddmuli  29032  adjlnop  29073  leopmul  29121  leoptr  29124  pjimai  29163  atcv1  29367  atexch  29368  atcvatlem  29372  fcoinvbr  29545  divnumden2  29692  xdivmul  29761  resvsca  29958  hasheuni  30275  difelsiga  30324  cndprobin  30624  bayesth  30629  sgn3da  30731  breprexplemc  30838  lediv2aALT  31697  subdivcomb1  31737  fununiq  31793  dfrdg2  31825  sltres  31940  sletr  32008  clsun  32448  neiin  32452  rdgeqoa  33348  curfv  33519  matunitlindflem1  33535  poimirlem32  33571  ftc1anclem4  33618  areacirc  33635  filbcmb  33665  ismtybnd  33736  grpoeqdivid  33810  ghomco  33820  rngonegrmul  33873  zerdivemp1x  33876  rngohomco  33903  rngoisoco  33911  riscer  33917  intidl  33958  isfldidl  33997  lshpnelb  34589  opnlen0  34793  opcon3b  34801  opcon2b  34802  oplecon3b  34805  opltcon3b  34809  opltcon2b  34811  oldmm1  34822  oldmm4  34825  oldmj1  34826  oldmj4  34829  cvrval2  34879  cvrcon3b  34882  leatb  34897  atcmp  34916  atcvreq0  34919  atlatle  34925  athgt  35060  3dim2  35072  islln2a  35121  lplnnleat  35146  lvolnleat  35187  4atlem10  35210  4atlem11  35213  4atlem12  35216  dalem21  35298  dalem22  35299  dalem23  35300  dalem29  35305  dalem30  35306  dalem31N  35307  dalem32  35308  dalem33  35309  dalem34  35310  dalem35  35311  dalem36  35312  dalem37  35313  dalem40  35316  dalem46  35322  dalem47  35323  dalem51  35327  dalem52  35328  dalem58  35334  dalem59  35335  pmaple  35365  paddclN  35446  pmapjoin  35456  pmapjat1  35457  elpcliN  35497  pclssN  35498  pclun2N  35503  2polcon4bN  35522  paddunN  35531  poldmj1N  35532  pmapj2N  35533  pmapocjN  35534  psubclinN  35552  paddatclN  35553  poml4N  35557  lautco  35701  ldilco  35720  ltrneq2  35752  trljat1  35771  cdlemc1  35796  cdleme10  35859  ltrnco  36324  trlcocnv  36325  trljco  36345  trljco2  36346  cdlemi1  36423  tendocnv  36627  diaord  36653  dibord  36765  dihord3  36863  dihord4  36864  dihmeetlem2N  36905  dihmeetlem4preN  36912  dochdmj1  36996  hdmap10lem  37448  mzprename  37629  dvdsrabdioph  37691  pell14qrdivcl  37746  monotoddzz  37825  jm2.19lem2  37874  jm2.19  37877  relexpaddss  38327  k0004lem3  38764  dvconstbi  38850  chordthmALT  39483  isosctrlem1ALT  39484  ssinc  39578  ssdec  39579  unima  39660  wessf1ornlem  39685  disjf1o  39692  disjinfi  39694  ssnnf1octb  39696  projf1o  39700  mapsnd  39702  mapssbi  39719  iunmapsn  39723  fvelimad  39772  upbdrech  39833  iuneqfzuzlem  39863  suplesup  39868  rexabslelem  39958  climxrrelem  40299  limsupresxr  40316  liminfresxr  40317  liminfvalxr  40333  cncfshift  40405  cncfperiod  40410  cncfuni  40417  icccncfext  40418  dvmptfprodlem  40477  dvnprodlem1  40479  itgspltprt  40513  ismbl3  40521  stoweidlem3  40538  stoweidlem10  40545  stoweidlem19  40554  stoweidlem31  40566  stoweidlem34  40569  stoweidlem44  40579  fourierdlem41  40683  fourierdlem42  40684  fourierdlem51  40692  fourierdlem68  40709  fourierdlem89  40730  fourierdlem91  40732  fourierdlem92  40733  fourierdlem94  40735  etransclem24  40793  etransclem34  40803  rrxdsfi  40823  qndenserrnbllem  40832  salincl  40861  saldifcl2  40864  subsalsal  40895  sge0pr  40929  sge0pnffigt  40931  sge0reuz  40982  nnfoctbdjlem  40990  nnfoctbdj  40991  meadjiunlem  41000  caratheodorylem2  41062  hoidmv1le  41129  hoidmvlelem3  41132  hspmbllem2  41162  opnvonmbllem2  41168  sssmf  41268  smfaddlem1  41292  sigaraf  41363  sigarmf  41364  nltle2tri  41648  subsubelfzo0  41661  iccpartiltu  41683  icceuelpart  41697  pfxsuffeqwrdeq  41731  pfxsuff1eqwrdeq  41732  ccatpfx  41734  pfxpfx  41740  pfxccatin12lem1  41748  pfxccatpfx1  41752  pfxccatpfx2  41753  repswpfx  41761  pfxco  41763  proththd  41856  mogoldbblem  41954  bgoldbtbndlem2  42019  xpprsng  42435  nn0sumltlt  42453  invginvrid  42473  ply1sclrmsm  42496  linccl  42528  lincvalpr  42532  lincresunit3lem1  42593  lincresunit3  42595  fdivmpt  42659  nnolog2flm1  42709  dignnld  42722  digexp  42726  dignn0flhalflem1  42734  setrec2fun  42764  reccot  42827  rectan  42828
  Copyright terms: Public domain W3C validator