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

Theorem 3adant2 1078
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 1057 . 2 ((𝜑𝜃𝜓) → (𝜑𝜓))
2 3adant.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2syl 17 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384  w3a 1036
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 386  df-3an 1038
This theorem is referenced by:  3ad2ant1  1080  eupickb  2536  vtoclegft  3275  eqeu  3371  funopg  5910  fnco  5987  dff1o2  6129  fnimapr  6249  fvmptt  6286  fnreseql  6313  f1elima  6505  f13dfv  6515  f1ocnvfvb  6520  oprssov  6788  ordunel  7012  poxp  7274  wfrlem4  7403  smoiso  7444  oaord  7612  oaword  7614  omcan  7634  omwordri  7637  odi  7644  omeulem1  7647  oeord  7653  oecan  7654  oewordri  7657  oeordsuc  7659  nnaord  7684  nnaordr  7685  nndi  7688  nnaword  7692  nnmwordri  7701  erov  7829  ecopovtrn  7835  xpdom3  8043  mapxpen  8111  findcard  8184  indexfi  8259  suppr  8362  infpr  8394  r111  8623  tcrank  8732  acndom  8859  infdif2  9017  infxpdom  9018  cfeq0  9063  cfsuc  9064  cfflb  9066  cflim2  9070  cfsmolem  9077  axcc3  9245  domtriomlem  9249  axdc3lem2  9258  axdc3lem4  9260  axdc4lem  9262  axcclem  9264  pwcfsdom  9390  tsktrss  9568  tsksuc  9569  tskuni  9590  adderpqlem  9761  mulerpqlem  9762  mulcanenq  9767  distrnq  9768  ltsonq  9776  ltanq  9778  ltmnq  9779  distrlem1pr  9832  distrlem5pr  9834  ltsopr  9839  ltsosr  9900  ltasr  9906  adddir  10016  axlttrn  10095  letr  10116  nnncan1  10302  npncan3  10304  pnpcan2  10306  subdi  10448  subdir  10449  mulcan1g  10665  mulcan2g  10666  divmul  10673  div23  10689  div13  10691  muldivdir  10705  divsubdir  10706  divcan7  10719  ltmul2  10859  lemul1  10860  lemul2  10861  lemul2a  10863  lediv1  10873  ltmuldiv2  10882  lemuldiv  10888  lemuldiv2  10889  ltdiv2  10894  lediv2  10898  fiminre  10957  infrelb  10993  nndivtr  11047  bndndx  11276  nn0n0n1ge2  11343  fnn0ind  11461  addlelt  11927  xrletr  11974  qsqueeze  12017  xleadd2a  12069  xleadd1  12070  xltadd2  12072  xltmul2  12108  supxrbnd  12143  iooneg  12277  iccneg  12278  icoshft  12279  icoshftf1o  12280  zltaddlt1le  12309  fzen  12343  uzsubsubfz  12348  ssfzunsnext  12371  fzrevral2  12410  fzshftral  12412  fz0fzdiffz0  12432  elfzmlbp  12434  elfzo  12456  nelfzo  12459  fzoaddel2  12507  fzosubel2  12511  elfzom1p1elfzo  12531  ssfzo12bi  12547  fzonfzoufzol  12555  subfzo0  12573  flltdivnn0lt  12617  modmulnn  12671  modcyc  12688  modaddabs  12691  modaddmod  12692  modmuladd  12695  modadd2mod  12703  modsubmod  12711  modsubmodmod  12712  modaddmodup  12716  modmulmod  12718  moddi  12721  modsubdir  12722  modfzo0difsn  12725  modsumfzodifsn  12726  uzindi  12764  axdc4uzlem  12765  expneg2  12852  expdiv  12894  expubnd  12904  mulbinom2  12967  bernneq2  12974  hashinfxadd  13157  brfi1indlem  13261  ccatval3  13346  ccatsymb  13349  ccatfv0  13350  ccatval1lsw  13351  ccats1val2  13386  swrdnd  13414  2swrd1eqwrdeq  13436  swrdswrd  13442  wrd2ind  13459  swrdccatin1  13464  swrdccatin12lem2b  13467  swrdccatin2  13468  swrdccatin12lem2  13470  swrdccatin12lem3  13471  swrdccat  13474  swrdccat3a  13475  swrdccat3blem  13476  repswswrd  13512  repswccat  13513  cshwidxmod  13530  2cshw  13540  3cshw  13545  scshwfzeqfzo  13553  cshwcsh2id  13555  cshimadifsn  13556  cshimadifsn0  13557  ccatco  13562  cshco  13563  swrdco  13564  lswco  13565  swrds2  13666  2swrd2eqwrdeq  13677  shftuz  13790  shftval2  13796  abs3dif  14052  fsumdifsnconst  14504  modfsummods  14506  sin02gt0  14903  dvdsval2  14967  dvdscmul  14989  dvdsmulc  14990  dvdscmulr  14991  dvdsmulcr  14992  mulmoddvds  15032  divalglem8  15104  ndvdssub  15114  rpmulgcd  15256  coprmdvdsOLD  15348  coprmprod  15356  cncongr1  15362  cncongr2  15363  isprm3  15377  modprm0  15491  coprimeprodsq  15494  pythagtriplem12  15512  pythagtriplem14  15514  pcprendvds  15526  pcmul  15537  pcdiv  15538  pcqcl  15542  pcqdiv  15543  pcdvdsb  15554  pcgcd  15563  vdwnnlem1  15680  hashbcss  15689  cshwshashlem1  15783  fvsetsid  15871  setsstruct2  15877  setsstruct  15879  mrcss  16257  mrcsscl  16261  mrcun  16263  cofulid  16531  catcisolem  16737  funcsetcestrclem9  16784  latleeqj1  17044  lubun  17104  clatleglb  17107  pslem  17187  dirtr  17217  mgmb1mgm1  17235  pwspjmhm  17349  gsumccat  17359  grpinvid1  17451  grpinvid2  17452  grpasscan1  17459  grpasscan2  17460  grpinvadd  17474  grpsubf  17475  grpsubrcan  17477  grpinvsub  17478  grpsubeq0  17482  grpsubadd0sub  17483  grppncan  17487  grpnpcan  17488  mulgnn0p1  17533  mulgaddcomlem  17544  mulginvcom  17546  mulginvinv  17547  subgsubcl  17586  subgsub  17587  eqglact  17626  qussub  17635  ghmsub  17649  psgnunilem4  17898  oddvds2  17964  odsubdvds  17967  gexnnod  17984  slwn0  18011  gsumdixp  18590  dvrcl  18667  unitdvcl  18668  dvrcan1  18672  dvrcan3  18673  dvreq1  18674  subrgdv  18778  abvsubtri  18816  idsrngd  18843  lmodvsubval2  18899  lsmcl  19064  lsmsp2  19068  lspsntrim  19079  lidldvgen  19236  evlslem4  19489  mpfsubrg  19513  ply1tmcl  19623  eqcoe1ply1eq  19648  gsummoncoe1  19655  lply1binomsc  19658  chrcong  19858  zndvds  19879  zntoslem  19886  ocvsscon  20000  obselocv  20053  frlmphl  20101  mamudm  20175  mamufacex  20176  scmatf1  20318  scmatf1o  20319  scmatrngiso  20323  submabas  20365  mdetdiaglem  20385  mdetralt2  20396  mdetero  20397  mdetunilem2  20400  mdetunilem6  20404  m2detleiblem7  20414  maducoeval2  20427  gsummatr01lem3  20444  gsummatr01  20446  smadiadetglem2  20459  cramerlem1  20474  mply1topmatcl  20591  mp2pm2mplem4  20595  ntrin  20846  elnei  20896  neindisj2  20908  ordtopn3  20981  ordtcld3  20984  leordtval2  20997  lecldbas  21004  cnrest2  21071  cmpsublem  21183  ptrescn  21423  xkococn  21444  kqfeq  21508  snfbas  21651  neifil  21665  fclsrest  21809  utopsnnei  22034  neipcfilu  22081  psmetsym  22096  psmetge0  22098  xmetge0  22130  xmetsym  22133  metustto  22339  metustbl  22352  restmetu  22356  nm2dif  22410  nmtri  22411  cnmet  22556  cnmpt2pc  22708  iihalf1  22711  iihalf2  22713  iocopnst  22720  clmnegsubdi2  22886  clmsub4  22887  clmvsubval2  22891  ncvspi  22937  cphsqrtcl3  22968  cph2ass  22994  cphipval2  23021  cphipval  23023  caublcls  23088  bcthlem3  23104  bcthlem4  23105  srabn  23137  rrxmet  23172  iblconst  23565  tdeglem3  23800  mdegmullem  23819  dvdsq1p  23901  coeid3  23977  aannenlem2  24065  pserdvlem2  24163  tanord1  24264  cxpef  24392  recxpcl  24402  logbchbase  24490  relogbcl  24492  relogbzcl  24493  logbleb  24502  logblt  24503  relogbcxpb  24506  lawcos  24527  pythag  24528  isosctrlem1  24529  isosctrlem2  24530  lgsmodeq  25048  lgsmulsqcoprm  25049  gausslemma2dlem1a  25071  2lgsoddprmlem2  25115  ax5seglem1  25789  axcontlem2  25826  axcontlem8  25832  upgrpredgv  26015  numedglnl  26020  issubgr2  26145  uhgrissubgr  26148  egrsubgr  26150  fusgrfisstep  26202  nbusgrfi  26257  nb3grprlem2  26264  cplgr3v  26312  cusgrsizeindslem  26328  finsumvtxdg2size  26427  rusgrpropadjvtx  26462  upgrwlkvtxedg  26522  usgr2trlncl  26637  uspgrn2crct  26681  crctcshwlkn0lem4  26686  crctcshwlkn0lem5  26687  wwlksnextproplem3  26787  umgr2adedgwlklem  26821  rusgr0edg  26849  clwlkclwwlklem2a4  26879  clwlkclwwlklem2a  26880  clwwlks1loop  26888  clwwlksn1loop  26889  clwwlksel  26894  clwwisshclwwslemlem  26906  erclwwlkstr  26916  erclwwlksntr  26928  clwlksfclwwlk  26942  uhgr3cyclex  27022  umgr3cyclex  27023  eucrctshift  27083  frgr3v  27119  3cyclfrgrrn  27130  numclwlk3lem3  27180  numclwwlkovf2ex  27191  extwwlkfab  27194  numclwwlk5  27216  numclwwlk6  27218  isgrpo  27321  grpoinvid1  27352  grpoinvid2  27353  grpoinvop  27357  grpodivinv  27360  grpoinvdiv  27361  grpodivf  27362  grponpcan  27367  ablonncan  27381  nvmval  27467  nvmval2  27468  nvmfval  27469  nvmul0or  27475  nvpncan2  27478  nvaddsub4  27482  nvmeq0  27483  nvdif  27491  nvpi  27492  nvmtri  27496  nvabs  27497  imsmetlem  27515  ipval2lem3  27530  ipval2  27532  4ipval2  27533  ipval3  27534  nmooge0  27592  blometi  27628  hvaddsub12  27865  hvsubdistr1  27876  hvsubdistr2  27877  hvaddcan2  27898  hvmulcan  27899  hvmulcan2  27900  hvsubcan  27901  hvsubcan2  27902  his7  27917  his2sub  27919  his2sub2  27920  norm3dif2  27978  shsubcl  28047  hhssnv  28091  shlej2  28190  fh2  28448  cm2j  28449  pjoi0  28546  hodcl  28576  hosubdi  28637  unopf1o  28745  unopadj  28748  adj2  28763  braadd  28774  bramul  28775  lnopaddmuli  28802  lnopsubmuli  28804  homco2  28806  lnfnaddmuli  28874  adjlnop  28915  leopmul  28963  leoptr  28966  pjimai  29005  atcv1  29209  atexch  29210  atcvatlem  29214  fcoinvbr  29391  divnumden2  29538  xdivmul  29607  resvsca  29804  hasheuni  30121  difelsiga  30170  cndprobin  30470  bayesth  30475  sgn3da  30577  breprexplemc  30684  lediv2aALT  31545  subdivcomb1  31586  fununiq  31643  dfrdg2  31675  sltres  31789  sletr  31857  clsun  32298  neiin  32302  rdgeqoa  33189  curfv  33360  matunitlindflem1  33376  poimirlem32  33412  ftc1anclem4  33459  areacirc  33476  filbcmb  33506  ismtybnd  33577  grpoeqdivid  33651  ghomco  33661  rngonegrmul  33714  zerdivemp1x  33717  rngohomco  33744  rngoisoco  33752  riscer  33758  intidl  33799  isfldidl  33838  lshpnelb  34090  opnlen0  34294  opcon3b  34302  opcon2b  34303  oplecon3b  34306  opltcon3b  34310  opltcon2b  34312  oldmm1  34323  oldmm4  34326  oldmj1  34327  oldmj4  34330  cvrval2  34380  cvrcon3b  34383  leatb  34398  atcmp  34417  atcvreq0  34420  atlatle  34426  athgt  34561  3dim2  34573  islln2a  34622  lplnnleat  34647  lvolnleat  34688  4atlem10  34711  4atlem11  34714  4atlem12  34717  dalem21  34799  dalem22  34800  dalem23  34801  dalem29  34806  dalem30  34807  dalem31N  34808  dalem32  34809  dalem33  34810  dalem34  34811  dalem35  34812  dalem36  34813  dalem37  34814  dalem40  34817  dalem46  34823  dalem47  34824  dalem51  34828  dalem52  34829  dalem58  34835  dalem59  34836  pmaple  34866  paddclN  34947  pmapjoin  34957  pmapjat1  34958  elpcliN  34998  pclssN  34999  pclun2N  35004  2polcon4bN  35023  paddunN  35032  poldmj1N  35033  pmapj2N  35034  pmapocjN  35035  psubclinN  35053  paddatclN  35054  poml4N  35058  lautco  35202  ldilco  35221  ltrneq2  35253  trljat1  35272  cdlemc1  35297  cdleme10  35360  ltrnco  35826  trlcocnv  35827  trljco  35847  trljco2  35848  cdlemi1  35925  tendocnv  36129  diaord  36155  dibord  36267  dihord3  36365  dihord4  36366  dihmeetlem2N  36407  dihmeetlem4preN  36414  dochdmj1  36498  hdmap10lem  36950  mzprename  37131  dvdsrabdioph  37193  pell14qrdivcl  37248  monotoddzz  37327  jm2.19lem2  37376  jm2.19  37379  relexpaddss  37829  k0004lem3  38267  dvconstbi  38353  chordthmALT  38989  isosctrlem1ALT  38990  ssinc  39084  ssdec  39085  unima  39162  wessf1ornlem  39187  disjf1o  39194  disjinfi  39196  ssnnf1octb  39198  projf1o  39202  mapsnd  39204  mapssbi  39221  iunmapsn  39225  fvelimad  39274  upbdrech  39332  iuneqfzuzlem  39363  suplesup  39368  rexabslelem  39458  limsupresxr  39792  liminfresxr  39793  liminfvalxr  39809  cncfshift  39850  cncfperiod  39855  cncfuni  39862  icccncfext  39863  dvmptfprodlem  39922  dvnprodlem1  39924  itgspltprt  39958  ismbl3  39966  stoweidlem3  39983  stoweidlem10  39990  stoweidlem19  39999  stoweidlem31  40011  stoweidlem34  40014  stoweidlem44  40024  fourierdlem41  40128  fourierdlem42  40129  fourierdlem51  40137  fourierdlem68  40154  fourierdlem89  40175  fourierdlem91  40177  fourierdlem92  40178  fourierdlem94  40180  etransclem24  40238  etransclem34  40248  rrxdsfi  40268  qndenserrnbllem  40277  salincl  40306  saldifcl2  40309  subsalsal  40340  sge0pr  40374  sge0pnffigt  40376  sge0reuz  40427  nnfoctbdjlem  40435  nnfoctbdj  40436  meadjiunlem  40445  caratheodorylem2  40504  hoidmv1le  40571  hoidmvlelem3  40574  hspmbllem2  40604  opnvonmbllem2  40610  sssmf  40710  smfaddlem1  40734  sigaraf  40805  sigarmf  40806  nltle2tri  41086  subsubelfzo0  41099  iccpartiltu  41122  icceuelpart  41136  pfxsuffeqwrdeq  41171  pfxsuff1eqwrdeq  41172  ccatpfx  41174  pfxpfx  41180  pfxccatin12lem1  41188  pfxccatpfx1  41192  pfxccatpfx2  41193  repswpfx  41201  pfxco  41203  proththd  41296  mogoldbblem  41394  bgoldbtbndlem2  41459  xpprsng  41875  nn0sumltlt  41893  invginvrid  41913  ply1sclrmsm  41936  linccl  41968  lincvalpr  41972  lincresunit3lem1  42033  lincresunit3  42035  fdivmpt  42099  nnolog2flm1  42149  dignnld  42162  digexp  42166  dignn0flhalflem1  42174  setrec2fun  42204  reccot  42264  rectan  42265
  Copyright terms: Public domain W3C validator