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

Theorem 3adant2 1072
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 1051 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030
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  df-3an 1032
This theorem is referenced by:  3ad2ant1  1074  eupickb  2525  vtoclegft  3252  eqeu  3343  funopg  5821  fnco  5898  dff1o2  6039  fnimapr  6156  fvmptt  6192  fnreseql  6219  f1elima  6398  f13dfv  6407  f1ocnvfvb  6412  oprssov  6678  ordunel  6896  poxp  7153  wfrlem4  7282  smoiso  7323  oaord  7491  oaword  7493  omcan  7513  omwordri  7516  odi  7523  omeulem1  7526  oeord  7532  oecan  7533  oewordri  7536  oeordsuc  7538  nnaord  7563  nnaordr  7564  nndi  7567  nnaword  7571  nnmwordri  7580  erov  7708  ecopovtrn  7714  xpdom3  7920  mapxpen  7988  findcard  8061  indexfi  8134  suppr  8237  infpr  8269  r111  8498  tcrank  8607  acndom  8734  infdif2  8892  infxpdom  8893  cfeq0  8938  cfsuc  8939  cfflb  8941  cflim2  8945  cfsmolem  8952  axcc3  9120  domtriomlem  9124  axdc3lem2  9133  axdc3lem4  9135  axdc4lem  9137  axcclem  9139  pwcfsdom  9261  tsktrss  9439  tsksuc  9440  tskuni  9461  adderpqlem  9632  mulerpqlem  9633  mulcanenq  9638  distrnq  9639  ltsonq  9647  ltanq  9649  ltmnq  9650  distrlem1pr  9703  distrlem5pr  9705  ltsopr  9710  ltsosr  9771  ltasr  9777  adddir  9887  axlttrn  9961  letr  9982  nnncan1  10168  npncan3  10170  pnpcan2  10172  subdi  10314  subdir  10315  mulcan1g  10531  mulcan2g  10532  divmul  10539  div23  10555  div13  10557  muldivdir  10571  divsubdir  10572  divcan7  10585  ltmul2  10725  lemul1  10726  lemul2  10727  lemul2a  10729  lediv1  10739  ltmuldiv2  10748  lemuldiv  10754  lemuldiv2  10755  ltdiv2  10760  lediv2  10764  fiminre  10823  infrelb  10857  nndivtr  10911  bndndx  11140  nn0n0n1ge2  11207  fnn0ind  11310  addlelt  11776  xrletr  11826  qsqueeze  11867  xleadd2a  11915  xleadd1  11916  xltadd2  11918  xltmul2  11954  supxrbnd  11988  iooneg  12121  iccneg  12122  icoshft  12123  icoshftf1o  12124  zltaddlt1le  12153  fzen  12186  uzsubsubfz  12191  fzrevral2  12252  fzshftral  12254  fz0fzdiffz0  12274  elfzmlbp  12276  elfzo  12298  nelfzo  12301  fzoaddel2  12348  fzosubel2  12352  elfzom1p1elfzo  12371  ssfzo12bi  12386  fzonfzoufzol  12394  subfzo0  12409  flltdivnn0lt  12453  modmulnn  12507  modcyc  12524  modaddabs  12527  modaddmod  12528  modmuladd  12531  modadd2mod  12539  modsubmod  12547  modsubmodmod  12548  modaddmodup  12552  modmulmod  12554  moddi  12557  modsubdir  12558  modfzo0difsn  12561  modsumfzodifsn  12562  uzindi  12600  axdc4uzlem  12601  expneg2  12688  expdiv  12730  expubnd  12740  mulbinom2  12803  bernneq2  12810  hashinfxadd  12989  brfi1indlem  13081  ccatval3  13164  ccatsymb  13167  ccatfv0  13168  ccatval1lsw  13169  ccats1val2  13204  swrdnd  13232  2swrd1eqwrdeq  13254  swrdswrd  13260  wrd2ind  13277  swrdccatin1  13282  swrdccatin12lem2b  13285  swrdccatin2  13286  swrdccatin12lem2  13288  swrdccatin12lem3  13289  swrdccat  13292  swrdccat3a  13293  swrdccat3blem  13294  repswswrd  13330  repswccat  13331  cshwidxmod  13348  2cshw  13358  3cshw  13363  scshwfzeqfzo  13371  cshwcsh2id  13373  cshimadifsn  13374  cshimadifsn0  13375  ccatco  13380  cshco  13381  swrdco  13382  lswco  13383  swrds2  13481  2swrd2eqwrdeq  13492  shftuz  13605  shftval2  13611  abs3dif  13867  modfsummods  14314  sin02gt0  14709  dvdsval2  14772  dvdscmul  14794  dvdsmulc  14795  dvdscmulr  14796  dvdsmulcr  14797  mulmoddvds  14837  divalglem8  14909  ndvdssub  14919  rpmulgcd  15061  coprmdvdsOLD  15153  coprmprod  15161  cncongr1  15167  cncongr2  15168  isprm3  15182  modprm0  15296  coprimeprodsq  15299  pythagtriplem12  15317  pythagtriplem14  15319  pcprendvds  15331  pcmul  15342  pcdiv  15343  pcqcl  15347  pcqdiv  15348  pcdvdsb  15359  pcgcd  15368  vdwnnlem1  15485  hashbcss  15494  cshwshashlem1  15588  fvsetsid  15670  mrcss  16047  mrcsscl  16051  mrcun  16053  cofulid  16321  catcisolem  16527  funcsetcestrclem9  16574  latleeqj1  16834  lubun  16894  clatleglb  16897  pslem  16977  dirtr  17007  mgmb1mgm1  17025  pwspjmhm  17139  gsumccat  17149  grpinvid1  17241  grpinvid2  17242  grpasscan1  17249  grpasscan2  17250  grpinvadd  17264  grpsubf  17265  grpsubrcan  17267  grpinvsub  17268  grpsubeq0  17272  grpsubadd0sub  17273  grppncan  17277  grpnpcan  17278  mulgnn0p1  17323  mulgaddcomlem  17334  mulginvcom  17336  mulginvinv  17337  subgsubcl  17376  subgsub  17377  eqglact  17416  qussub  17425  ghmsub  17439  psgnunilem4  17688  oddvds2  17754  odsubdvds  17757  gexnnod  17774  slwn0  17801  gsumdixp  18380  dvrcl  18457  unitdvcl  18458  dvrcan1  18462  dvrcan3  18463  dvreq1  18464  subrgdv  18568  abvsubtri  18606  idsrngd  18633  lmodvsubval2  18689  lsmcl  18852  lsmsp2  18856  lspsntrim  18867  lidldvgen  19024  evlslem4  19277  mpfsubrg  19301  ply1tmcl  19411  eqcoe1ply1eq  19436  gsummoncoe1  19443  lply1binomsc  19446  chrcong  19643  zndvds  19664  zntoslem  19671  ocvsscon  19785  obselocv  19838  frlmphl  19886  mamudm  19960  mamufacex  19961  scmatf1  20103  scmatf1o  20104  scmatrngiso  20108  submabas  20150  mdetdiaglem  20170  mdetralt2  20181  mdetero  20182  mdetunilem2  20185  mdetunilem6  20189  m2detleiblem7  20199  maducoeval2  20212  gsummatr01lem3  20229  gsummatr01  20231  smadiadetglem2  20244  cramerlem1  20259  mply1topmatcl  20376  mp2pm2mplem4  20380  ntrin  20622  elnei  20672  neindisj2  20684  ordtopn3  20757  ordtcld3  20760  leordtval2  20773  lecldbas  20780  cnrest2  20847  cmpsublem  20959  ptrescn  21199  xkococn  21220  kqfeq  21284  snfbas  21427  neifil  21441  fclsrest  21585  utopsnnei  21810  neipcfilu  21857  psmetsym  21872  psmetge0  21874  xmetge0  21906  xmetsym  21909  metustto  22115  metustbl  22128  restmetu  22132  nm2dif  22186  nmtri  22187  cnmet  22332  cnmpt2pc  22482  iihalf1  22485  iihalf2  22487  iocopnst  22494  clmnegsubdi2  22660  clmsub4  22661  clmvsubval2  22665  ncvspi  22708  cphsqrtcl3  22739  cph2ass  22765  cphipval2  22792  cphipval  22794  caublcls  22859  bcthlem3  22875  bcthlem4  22876  srabn  22908  rrxmet  22943  iblconst  23334  tdeglem3  23567  mdegmullem  23586  dvdsq1p  23668  coeid3  23744  aannenlem2  23832  pserdvlem2  23930  tanord1  24031  cxpef  24155  recxpcl  24165  logbchbase  24253  relogbcl  24255  relogbzcl  24256  logbleb  24265  logblt  24266  relogbcxpb  24269  lawcos  24290  pythag  24291  isosctrlem1  24292  isosctrlem2  24293  lgsmodeq  24811  lgsmulsqcoprm  24812  gausslemma2dlem1a  24834  2lgsoddprmlem2  24878  ax5seglem1  25553  axcontlem2  25590  axcontlem8  25596  fiusgraedgfi  25729  nbgraf1olem3  25765  nb3graprlem2  25774  cusgra3v  25786  cusgrasizeindslem2  25796  cusgrasizeinds  25797  iswlkon  25855  istrlon  25864  2trllemE  25876  usgrwlknloop  25886  ispthon  25899  isspthon  25906  usgra2adedgwlkonALT  25937  usgrcyclnl2  25962  3v3e3cycl1  25965  constr3lem4  25968  constr3lem5  25969  constr3lem6  25970  constr3trllem2  25972  constr3trllem3  25973  4cycl4dv  25988  wwlkextproplem3  26064  clwwlkgt0  26092  clwwlknndef  26094  clwwlknfi  26099  clwlkisclwwlklem2a4  26105  clwlkisclwwlklem2a  26106  clwwlkel  26114  clwwlkext2edg  26123  clwwisshclwwlem1  26126  clwwnisshclwwn  26130  erclwwlktr  26136  erclwwlkntr  26148  clwlkfclwwlk  26164  clwlkfoclwwlk  26165  usg2wotspth  26204  2spontn0vne  26207  nbhashnn0  26234  nbhashuvtx  26236  usgrauvtxvdbi  26240  rusgra0edg  26275  frgra3v  26322  usg2spot2nb  26385  numclwlk3lem3  26393  extwwlkfablem2  26398  numclwwlkovf2ex  26406  numclwwlkovgelim  26409  numclwwlk4  26430  numclwwlk5lem  26431  numclwwlk5  26432  numclwwlk6  26433  numclwwlk7  26434  isgrpo  26528  grpoinvid1  26559  grpoinvid2  26560  grpoinvop  26564  grpodivinv  26567  grpoinvdiv  26568  grpodivf  26569  grponpcan  26574  ablonncan  26588  nvmval  26674  nvmval2  26675  nvmfval  26676  nvmul0or  26682  nvpncan2  26685  nvaddsub4  26689  nvmeq0  26690  nvdif  26698  nvpi  26699  nvmtri  26703  nvabs  26704  imsmetlem  26722  ipval2lem3  26737  ipval2  26739  4ipval2  26740  ipval3  26741  nmooge0  26799  blometi  26835  hvaddsub12  27072  hvsubdistr1  27083  hvsubdistr2  27084  hvaddcan2  27105  hvmulcan  27106  hvmulcan2  27107  hvsubcan  27108  hvsubcan2  27109  his7  27124  his2sub  27126  his2sub2  27127  norm3dif2  27185  shsubcl  27254  hhssnv  27298  shlej2  27397  fh2  27655  cm2j  27656  pjoi0  27753  hodcl  27783  hosubdi  27844  unopf1o  27952  unopadj  27955  adj2  27970  braadd  27981  bramul  27982  lnopaddmuli  28009  lnopsubmuli  28011  homco2  28013  lnfnaddmuli  28081  adjlnop  28122  leopmul  28170  leoptr  28173  pjimai  28212  atcv1  28416  atexch  28417  atcvatlem  28421  fcoinvbr  28592  divnumden2  28744  xdivmul  28757  resvsca  28954  hasheuni  29267  difelsiga  29316  cndprobin  29616  bayesth  29621  sgn3da  29723  lediv2aALT  30618  subdivcomb1  30657  fununiq  30706  dfrdg2  30738  sltres  30854  nobndlem8  30891  clsun  31286  neiin  31290  rdgeqoa  32177  curfv  32342  matunitlindflem1  32358  poimirlem32  32394  ftc1anclem4  32441  areacirc  32458  filbcmb  32488  ismtybnd  32559  grpoeqdivid  32633  ghomco  32643  rngonegrmul  32696  zerdivemp1x  32699  rngohomco  32726  rngoisoco  32734  riscer  32740  intidl  32781  isfldidl  32820  lshpnelb  33072  opnlen0  33276  opcon3b  33284  opcon2b  33285  oplecon3b  33288  opltcon3b  33292  opltcon2b  33294  oldmm1  33305  oldmm4  33308  oldmj1  33309  oldmj4  33312  cvrval2  33362  cvrcon3b  33365  leatb  33380  atcmp  33399  atcvreq0  33402  atlatle  33408  athgt  33543  3dim2  33555  islln2a  33604  lplnnleat  33629  lvolnleat  33670  4atlem10  33693  4atlem11  33696  4atlem12  33699  dalem21  33781  dalem22  33782  dalem23  33783  dalem29  33788  dalem30  33789  dalem31N  33790  dalem32  33791  dalem33  33792  dalem34  33793  dalem35  33794  dalem36  33795  dalem37  33796  dalem40  33799  dalem46  33805  dalem47  33806  dalem51  33810  dalem52  33811  dalem58  33817  dalem59  33818  pmaple  33848  paddclN  33929  pmapjoin  33939  pmapjat1  33940  elpcliN  33980  pclssN  33981  pclun2N  33986  2polcon4bN  34005  paddunN  34014  poldmj1N  34015  pmapj2N  34016  pmapocjN  34017  psubclinN  34035  paddatclN  34036  poml4N  34040  lautco  34184  ldilco  34203  ltrneq2  34235  trljat1  34254  cdlemc1  34279  cdleme10  34342  ltrnco  34808  trlcocnv  34809  trljco  34829  trljco2  34830  cdlemi1  34907  tendocnv  35111  diaord  35137  dibord  35249  dihord3  35347  dihord4  35348  dihmeetlem2N  35389  dihmeetlem4preN  35396  dochdmj1  35480  hdmap10lem  35932  mzprename  36113  dvdsrabdioph  36175  pell14qrdivcl  36230  monotoddzz  36309  jm2.19lem2  36358  jm2.19  36361  relexpaddss  36812  k0004lem3  37250  dvconstbi  37338  chordthmALT  37974  isosctrlem1ALT  37975  ssinc  38075  ssdec  38076  eliuniin  38090  eliuniin2  38118  unima  38123  wessf1ornlem  38149  disjf1o  38156  disjinfi  38158  ssnnf1octb  38160  projf1o  38164  mapsnd  38166  mapssbi  38183  iunmapsn  38187  upbdrech  38243  iuneqfzuzlem  38274  suplesup  38279  cncfshift  38542  cncfperiod  38547  cncfuni  38555  icccncfext  38556  dvmptfprodlem  38617  dvnprodlem1  38619  itgspltprt  38654  ismbl3  38662  stoweidlem3  38679  stoweidlem10  38686  stoweidlem19  38695  stoweidlem31  38707  stoweidlem34  38710  stoweidlem44  38720  fourierdlem41  38824  fourierdlem42  38825  fourierdlem51  38833  fourierdlem68  38850  fourierdlem89  38871  fourierdlem91  38873  fourierdlem92  38874  fourierdlem94  38876  etransclem24  38934  etransclem34  38944  rrxdsfi  38964  qndenserrnbllem  38973  salincl  39002  saldifcl2  39005  subsalsal  39036  sge0pr  39070  sge0pnffigt  39072  sge0reuz  39123  nnfoctbdjlem  39131  nnfoctbdj  39132  meadjiunlem  39141  caratheodorylem2  39200  hoidmv1le  39267  hoidmvlelem3  39270  hspmbllem2  39300  opnvonmbllem2  39306  sssmf  39408  smfaddlem1  39432  sigaraf  39474  sigarmf  39475  nltle2tri  39726  iccpartiltu  39744  icceuelpart  39758  proththd  39853  bgoldbtbndlem2  40006  pfxsuffeqwrdeq  40053  pfxsuff1eqwrdeq  40054  ccatpfx  40056  pfxpfx  40062  pfxccatin12lem1  40070  pfxccatpfx1  40074  pfxccatpfx2  40075  repswpfx  40083  pfxco  40085  subsubelfzo0  40165  issubgr2  40477  uhgrissubgr  40480  egrsubgr  40482  fusgrfisstep  40529  nbusgrfi  40583  nb3grprlem2  40590  cplgr3v  40638  cusgrsizeindslem  40648  rusgrpropadjvtx  40766  upgr1wlkvtxedg  40834  usgr2trlncl  40947  uspgrn2crct  40992  crctcsh1wlkn0lem4  40997  crctcsh1wlkn0lem5  40998  wwlksnextproplem3  41098  umgr2adedgwlklem  41132  rusgr0edg  41157  clwlkclwwlklem2a4  41187  clwlkclwwlklem2a  41188  clwwlks1loop  41196  clwwlksn1loop  41197  clwwlksel  41202  clwwisshclwwslemlem  41214  erclwwlkstr  41224  erclwwlksntr  41236  clwlksfclwwlk  41250  uhgr3cyclex  41330  umgr3cyclex  41331  eucrctshift  41392  frgr3v  41426  3cyclfrgrrn  41437  fusgr2wsp2nb  41479  av-numclwlk3lem3  41487  av-numclwwlkovf2ex  41498  av-extwwlkfab  41501  av-numclwwlk5  41523  av-numclwwlk6  41525  xpprsng  41884  nn0sumltlt  41902  invginvrid  41923  ply1sclrmsm  41946  linccl  41978  lincvalpr  41982  lincresunit3lem1  42043  lincresunit3  42045  fdivmpt  42113  nnolog2flm1  42163  dignnld  42176  digexp  42180  dignn0flhalflem1  42188  reccot  42240  rectan  42241
  Copyright terms: Public domain W3C validator