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

Theorem 3adant2 1125
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 3adant.1 . . 3 ((𝜑𝜓) → 𝜒)
21adantlr 694 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
323impa 1100 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1071
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 383  df-3an 1073
This theorem is referenced by:  3ad2ant1  1127  3simpb  1144  3imp3i2an  1436  eupickb  2687  vtoclegft  3431  eqeu  3529  funopg  6065  fnco  6139  dff1o2  6283  fnimapr  6404  fvmptt  6442  fnreseql  6470  f1elima  6663  f13dfv  6673  f1ocnvfvb  6678  oprssov  6950  ordunel  7174  poxp  7440  wfrlem4  7570  wfrlem4OLD  7571  smoiso  7612  oaord  7781  oaword  7783  omcan  7803  omwordri  7806  odi  7813  omeulem1  7816  oeord  7822  oecan  7823  oewordri  7826  oeordsuc  7828  nnaord  7853  nnaordr  7854  nndi  7857  nnaword  7861  nnmwordri  7870  erov  7997  ecopovtrn  8003  mapsnd  8051  xpdom3  8214  mapxpen  8282  findcard  8355  indexfi  8430  suppr  8533  infpr  8565  r111  8802  tcrank  8911  acndom  9074  infdif2  9234  infxpdom  9235  cfeq0  9280  cfsuc  9281  cfflb  9283  cflim2  9287  cfsmolem  9294  axcc3  9462  domtriomlem  9466  axdc3lem2  9475  axdc3lem4  9477  axdc4lem  9479  axcclem  9481  pwcfsdom  9607  tsktrss  9785  tsksuc  9786  tskuni  9807  adderpqlem  9978  mulerpqlem  9979  mulcanenq  9984  distrnq  9985  ltsonq  9993  ltanq  9995  ltmnq  9996  distrlem1pr  10049  distrlem5pr  10051  ltsopr  10056  ltsosr  10117  ltasr  10123  adddir  10233  axlttrn  10312  letr  10333  nnncan1  10519  npncan3  10521  pnpcan2  10523  subdi  10665  subdir  10666  mulcan1g  10882  mulcan2g  10883  divmul  10890  div23  10906  div13  10908  muldivdir  10922  divsubdir  10923  divcan7  10936  ltmul2  11076  lemul1  11077  lemul2  11078  lemul2a  11080  lediv1  11090  ltmuldiv2  11099  lemuldiv  11105  lemuldiv2  11106  ltdiv2  11111  lediv2  11115  fiminre  11174  infrelb  11210  nndivtr  11264  bndndx  11493  nn0n0n1ge2  11560  fnn0ind  11678  addlelt  12147  xrletr  12194  qsqueeze  12237  xleadd2a  12289  xleadd1  12290  xltadd2  12292  xltmul2  12328  supxrbnd  12363  iooneg  12499  iccneg  12500  icoshft  12501  icoshftf1o  12502  zltaddlt1le  12531  fzen  12565  uzsubsubfz  12570  ssfzunsnext  12593  fzrevral2  12633  fzshftral  12635  fz0fzdiffz0  12656  elfzmlbp  12658  elfzo  12680  nelfzo  12683  fzoaddel2  12732  fzosubel2  12736  elfzom1p1elfzo  12756  ssfzo12bi  12771  fzonfzoufzol  12779  subfzo0  12798  flltdivnn0lt  12842  modmulnn  12896  modcyc  12913  modaddabs  12916  modaddmod  12917  modmuladd  12920  modadd2mod  12928  modsubmod  12936  modsubmodmod  12937  modaddmodup  12941  modmulmod  12943  moddi  12946  modsubdir  12947  modfzo0difsn  12950  modsumfzodifsn  12951  uzindi  12989  axdc4uzlem  12990  expneg2  13076  expdiv  13118  expubnd  13128  mulbinom2  13191  bernneq2  13198  hashinfxadd  13376  hashdifsnp1  13480  ccatval3  13561  ccatsymb  13564  ccatfv0  13565  ccatval1lsw  13566  ccats1val2  13610  swrdnd  13641  2swrd1eqwrdeq  13663  swrdswrd  13669  wrd2ind  13686  swrdccatin1  13692  swrdccatin12lem2b  13695  swrdccatin2  13696  swrdccatin12lem2  13698  swrdccatin12lem3  13699  swrdccat  13702  swrdccat3a  13703  swrdccat3blem  13704  repswswrd  13740  repswccat  13741  cshwidxmod  13758  2cshw  13768  3cshw  13773  scshwfzeqfzo  13781  cshwcsh2id  13783  cshimadifsn  13784  cshimadifsn0  13785  ccatco  13790  cshco  13791  swrdco  13792  lswco  13793  swrds2  13894  2swrd2eqwrdeq  13906  shftuz  14017  shftval2  14023  abs3dif  14279  fsumdifsnconst  14730  modfsummods  14732  sin02gt0  15128  dvdsval2  15192  dvdscmul  15217  dvdsmulc  15218  dvdscmulr  15219  dvdsmulcr  15220  divalglem8  15331  ndvdssub  15341  rpmulgcd  15483  coprmprod  15582  cncongr1  15588  cncongr2  15589  isprm3  15603  modprm0  15717  coprimeprodsq  15720  pythagtriplem12  15738  pythagtriplem14  15740  pcprendvds  15752  pcmul  15763  pcdiv  15764  pcqcl  15768  pcqdiv  15769  pcdvdsb  15780  pcgcd  15789  vdwnnlem1  15906  hashbcss  15915  cshwshashlem1  16009  fvsetsid  16097  setsstruct2  16103  setsstruct  16105  mrcss  16484  mrcsscl  16488  mrcun  16490  cofulid  16757  catcisolem  16963  funcsetcestrclem9  17011  latleeqj1  17271  lubun  17331  clatleglb  17334  pslem  17414  dirtr  17444  mgmb1mgm1  17462  pwspjmhm  17576  gsumccat  17586  grpinvid1  17678  grpinvid2  17679  grpasscan1  17686  grpasscan2  17687  grpinvadd  17701  grpsubf  17702  grpsubrcan  17704  grpinvsub  17705  grpsubeq0  17709  grpsubadd0sub  17710  grppncan  17714  grpnpcan  17715  mulgnn0p1  17760  mulgaddcomlem  17771  mulginvcom  17773  mulginvinv  17774  subgsubcl  17813  subgsub  17814  eqglact  17853  qussub  17862  ghmsub  17876  psgnunilem4  18124  oddvds2  18190  odsubdvds  18193  gexnnod  18210  slwn0  18237  gsumdixp  18817  dvrcl  18894  unitdvcl  18895  dvrcan1  18899  dvrcan3  18900  dvreq1  18901  subrgdv  19007  abvsubtri  19045  idsrngd  19072  lmodvsubval2  19128  lsmcl  19296  lsmsp2  19300  lspsntrim  19311  lidldvgen  19470  evlslem4  19723  mpfsubrg  19747  ply1tmcl  19857  eqcoe1ply1eq  19882  gsummoncoe1  19889  lply1binomsc  19892  chrcong  20092  zndvds  20113  zntoslem  20120  ocvsscon  20236  obselocv  20289  frlmphl  20337  mamudm  20411  mamufacex  20412  scmatf1  20555  scmatf1o  20556  scmatrngiso  20560  submabas  20602  mdetdiaglem  20622  mdetralt2  20633  mdetero  20634  mdetunilem2  20637  mdetunilem6  20641  m2detleiblem7  20651  maducoeval2  20664  gsummatr01lem3  20682  gsummatr01  20684  smadiadetglem2  20697  cramerlem1  20713  mply1topmatcl  20830  mp2pm2mplem4  20834  ntrin  21086  elnei  21136  neindisj2  21148  ordtopn3  21221  ordtcld3  21224  leordtval2  21237  lecldbas  21244  cnrest2  21311  cmpsublem  21423  ptrescn  21663  xkococn  21684  kqfeq  21748  snfbas  21890  neifil  21904  fclsrest  22048  utopsnnei  22273  neipcfilu  22320  psmetsym  22335  psmetge0  22337  xmetge0  22369  xmetsym  22372  metustto  22578  metustbl  22591  restmetu  22595  nm2dif  22649  nmtri  22650  cnmet  22795  cnmpt2pc  22947  iihalf1  22950  iihalf2  22952  iocopnst  22959  clmnegsubdi2  23124  clmsub4  23125  clmvsubval2  23129  ncvspi  23175  cphsqrtcl3  23206  cph2ass  23232  cphipval2  23259  cphipval  23261  caublcls  23326  bcthlem3  23342  bcthlem4  23343  srabn  23375  rrxmet  23410  iblconst  23804  tdeglem3  24039  mdegmullem  24058  dvdsq1p  24140  coeid3  24216  aannenlem2  24304  pserdvlem2  24402  tanord1  24504  cxpef  24632  recxpcl  24642  logbchbase  24730  relogbcl  24732  relogbzcl  24733  logbleb  24742  logblt  24743  relogbcxpb  24746  lawcos  24767  pythag  24768  isosctrlem1  24769  isosctrlem2  24770  lgsmodeq  25288  lgsmulsqcoprm  25289  gausslemma2dlem1a  25311  2lgsoddprmlem2  25355  ax5seglem1  26029  axcontlem2  26066  axcontlem8  26072  upgrpredgv  26256  numedglnl  26261  issubgr2  26387  uhgrissubgr  26390  egrsubgr  26392  fusgrfisstep  26444  nbusgrfi  26499  nb3grprlem2  26506  cplgr3v  26566  cusgrsizeindslem  26582  finsumvtxdg2size  26681  rusgrpropadjvtx  26716  upgrwlkvtxedg  26776  usgr2trlncl  26891  uspgrn2crct  26936  crctcshwlkn0lem4  26941  crctcshwlkn0lem5  26942  wwlksnextproplem3  27056  umgr2adedgwlklem  27091  rusgr0edg  27122  clwwlk1loop  27138  clwwlkccatlem  27139  clwlkclwwlklem2a4  27147  clwlkclwwlklem2a  27148  clwwisshclwwslemlem  27163  erclwwlktr  27172  clwwlkel  27202  erclwwlkntr  27229  clwlksfclwwlkOLD  27243  clwwlknonwwlknonbOLD  27282  clwwlknonex2lem2  27284  uhgr3cyclex  27362  umgr3cyclex  27363  eucrctshift  27423  frgr3v  27457  3cyclfrgrrn  27468  frgrwopreglem5a  27493  frgr2wsp1  27512  extwwlkfab  27538  clwwlknonclwlknonf1o  27549  clwwlknonclwlknonf1oOLD  27551  numclwwlk3lem1  27581  numclwwlk5  27587  numclwwlk6  27589  isgrpo  27691  grpoinvid1  27722  grpoinvid2  27723  grpoinvop  27727  grpodivinv  27730  grpoinvdiv  27731  grpodivf  27732  grponpcan  27737  ablonncan  27751  nvmval  27837  nvmval2  27838  nvmfval  27839  nvmul0or  27845  nvpncan2  27848  nvaddsub4  27852  nvmeq0  27853  nvdif  27861  nvpi  27862  nvmtri  27866  nvabs  27867  imsmetlem  27885  ipval2lem3  27900  ipval2  27902  4ipval2  27903  ipval3  27904  nmooge0  27962  blometi  27998  hvaddsub12  28235  hvsubdistr1  28246  hvsubdistr2  28247  hvaddcan2  28268  hvmulcan  28269  hvmulcan2  28270  hvsubcan  28271  hvsubcan2  28272  his7  28287  his2sub  28289  his2sub2  28290  norm3dif2  28348  shsubcl  28417  hhssnv  28461  shlej2  28560  fh2  28818  cm2j  28819  pjoi0  28916  hodcl  28946  hosubdi  29007  unopf1o  29115  unopadj  29118  adj2  29133  braadd  29144  bramul  29145  lnopaddmuli  29172  lnopsubmuli  29174  homco2  29176  lnfnaddmuli  29244  adjlnop  29285  leopmul  29333  leoptr  29336  pjimai  29375  atcv1  29579  atexch  29580  atcvatlem  29584  fcoinvbr  29757  divnumden2  29904  xdivmul  29973  resvsca  30170  hasheuni  30487  difelsiga  30536  cndprobin  30836  bayesth  30841  sgn3da  30943  breprexplemc  31050  lediv2aALT  31909  subdivcomb1  31949  fununiq  32005  dfrdg2  32037  sltres  32152  sletr  32220  clsun  32660  neiin  32664  rdgeqoa  33555  curfv  33722  matunitlindflem1  33738  poimirlem32  33774  ftc1anclem4  33820  areacirc  33837  filbcmb  33867  ismtybnd  33938  grpoeqdivid  34012  ghomco  34022  rngonegrmul  34075  zerdivemp1x  34078  rngohomco  34105  rngoisoco  34113  riscer  34119  intidl  34160  isfldidl  34199  lshpnelb  34793  opnlen0  34997  opcon3b  35005  opcon2b  35006  oplecon3b  35009  opltcon3b  35013  opltcon2b  35015  oldmm1  35026  oldmm4  35029  oldmj1  35030  oldmj4  35033  cvrval2  35083  cvrcon3b  35086  leatb  35101  atcmp  35120  atcvreq0  35123  atlatle  35129  athgt  35264  3dim2  35276  islln2a  35325  lplnnleat  35350  lvolnleat  35391  4atlem10  35414  4atlem11  35417  4atlem12  35420  dalem21  35502  dalem22  35503  dalem23  35504  dalem29  35509  dalem30  35510  dalem31N  35511  dalem32  35512  dalem33  35513  dalem34  35514  dalem35  35515  dalem36  35516  dalem37  35517  dalem40  35520  dalem46  35526  dalem47  35527  dalem51  35531  dalem52  35532  dalem58  35538  dalem59  35539  pmaple  35569  paddclN  35650  pmapjoin  35660  pmapjat1  35661  elpcliN  35701  pclssN  35702  pclun2N  35707  2polcon4bN  35726  paddunN  35735  poldmj1N  35736  pmapj2N  35737  pmapocjN  35738  psubclinN  35756  paddatclN  35757  poml4N  35761  lautco  35905  ldilco  35924  ltrneq2  35956  trljat1  35975  cdlemc1  36000  cdleme10  36063  ltrnco  36528  trlcocnv  36529  trljco  36549  trljco2  36550  cdlemi1  36627  tendocnv  36831  diaord  36857  dibord  36969  dihord3  37067  dihord4  37068  dihmeetlem2N  37109  dihmeetlem4preN  37116  dochdmj1  37200  hdmap10lem  37649  mzprename  37838  dvdsrabdioph  37900  pell14qrdivcl  37955  monotoddzz  38034  jm2.19lem2  38083  jm2.19  38086  relexpaddss  38536  k0004lem3  38973  dvconstbi  39059  chordthmALT  39691  isosctrlem1ALT  39692  ssinc  39785  ssdec  39786  unima  39866  wessf1ornlem  39891  disjf1o  39898  disjinfi  39900  ssnnf1octb  39902  projf1o  39906  mapssbi  39923  iunmapsn  39927  fvelimad  39976  upbdrech  40036  iuneqfzuzlem  40066  suplesup  40071  rexabslelem  40161  climxrrelem  40499  limsupresxr  40516  liminfresxr  40517  liminfvalxr  40533  cncfshift  40605  cncfperiod  40610  cncfuni  40617  icccncfext  40618  dvmptfprodlem  40677  dvnprodlem1  40679  itgspltprt  40712  ismbl3  40720  stoweidlem3  40737  stoweidlem10  40744  stoweidlem19  40753  stoweidlem31  40765  stoweidlem34  40768  stoweidlem44  40778  fourierdlem41  40882  fourierdlem42  40883  fourierdlem51  40891  fourierdlem68  40908  fourierdlem89  40929  fourierdlem91  40931  fourierdlem92  40932  fourierdlem94  40934  etransclem24  40992  etransclem34  41002  rrxdsfi  41022  qndenserrnbllem  41031  salincl  41060  saldifcl2  41063  subsalsal  41094  sge0pr  41128  sge0pnffigt  41130  sge0reuz  41181  nnfoctbdjlem  41189  nnfoctbdj  41190  meadjiunlem  41199  caratheodorylem2  41261  hoidmv1le  41328  hoidmvlelem3  41331  hspmbllem2  41361  opnvonmbllem2  41367  sssmf  41467  smfaddlem1  41491  sigaraf  41562  sigarmf  41563  nltle2tri  41851  subsubelfzo0  41864  iccpartiltu  41886  icceuelpart  41900  pfxsuffeqwrdeq  41934  pfxsuff1eqwrdeq  41935  ccatpfx  41937  pfxpfx  41943  pfxccatin12lem1  41951  pfxccatpfx1  41955  pfxccatpfx2  41956  repswpfx  41964  pfxco  41966  proththd  42059  mogoldbblem  42157  bgoldbtbndlem2  42222  xpprsng  42638  nn0sumltlt  42656  invginvrid  42676  ply1sclrmsm  42699  linccl  42731  lincvalpr  42735  lincresunit3lem1  42796  lincresunit3  42798  fdivmpt  42862  nnolog2flm1  42912  dignnld  42925  digexp  42929  dignn0flhalflem1  42937  setrec2fun  42967  reccot  43030  rectan  43031
  Copyright terms: Public domain W3C validator