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

Theorem 3adant2 1123
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 711 . 2 (((𝜑𝜃) ∧ 𝜓) → 𝜒)
323impa 1102 1 ((𝜑𝜃𝜓) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1079
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 208  df-an 397  df-3an 1081
This theorem is referenced by:  3ad2ant1  1125  3simpb  1141  3imp3i2an  1337  eupickb  2713  vtoclegft  3579  eqeu  3694  iotan0  6338  funopg  6382  fnco  6458  dff1o2  6613  fvelimad  6725  unima  6732  fnimapr  6740  fvmptt  6780  fnreseql  6810  xpprsng  6894  f1elima  7012  f13dfv  7022  f1ocnvfvb  7027  oprssov  7306  funelss  7735  poxp  7811  wfrlem4  7947  smoiso  7988  oaord  8162  oaword  8164  omcan  8184  omwordri  8187  odi  8194  omeulem1  8197  oeord  8203  oecan  8204  oewordri  8207  oeordsuc  8209  nnaord  8234  nnaordr  8235  nndi  8238  nnaword  8242  nnmwordri  8251  erov  8383  ecopovtrn  8389  mapsnd  8438  xpdom3  8603  mapxpen  8671  findcard  8745  indexfi  8820  suppr  8923  infpr  8955  r111  9192  tcrank  9301  acndom  9465  infdif2  9620  infxpdom  9621  cfeq0  9666  cfsuc  9667  cfflb  9669  cflim2  9673  cfsmolem  9680  axcc3  9848  domtriomlem  9852  axdc3lem2  9861  axdc3lem4  9863  axdc4lem  9865  axcclem  9867  pwcfsdom  9993  tsktrss  10171  tsksuc  10172  tskuni  10193  adderpqlem  10364  mulerpqlem  10365  mulcanenq  10370  distrnq  10371  ltsonq  10379  ltanq  10381  ltmnq  10382  distrlem1pr  10435  distrlem5pr  10437  ltsopr  10442  ltsosr  10504  ltasr  10510  adddir  10620  axlttrn  10701  letr  10722  nnncan1  10910  npncan3  10912  pnpcan2  10914  subdi  11061  subdir  11062  mulcan1g  11281  mulcan2g  11282  divmul  11289  div23  11305  div13  11307  muldivdir  11321  divsubdir  11322  subdivcomb1  11323  divcan7  11337  ltmul2  11479  lemul1  11480  lemul2  11481  lemul2a  11483  lediv1  11493  ltmuldiv2  11502  lemuldiv  11508  lemuldiv2  11509  ltdiv2  11514  lediv2  11518  fiminreOLD  11578  infrelb  11614  nndivtr  11672  bndndx  11884  nn0n0n1ge2  11950  fnn0ind  12069  addlelt  12491  xrletr  12539  qsqueeze  12582  xleadd2a  12635  xleadd1  12636  xltadd2  12638  xltmul2  12674  supxrbnd  12709  iooneg  12845  iccneg  12846  icoshft  12847  icoshftf1o  12848  zltaddlt1le  12878  fzen  12912  uzsubsubfz  12917  ssfzunsnext  12940  fzrevral2  12981  fzshftral  12983  fz0fzdiffz0  13004  elfzmlbp  13006  elfzo  13028  nelfzo  13031  fzoaddel2  13081  fzosubel2  13085  ssfzo12bi  13120  fzonfzoufzol  13128  subfzo0  13147  flltdivnn0lt  13191  modmulnn  13245  modcyc  13262  modaddabs  13265  modaddmod  13266  modmuladd  13269  modadd2mod  13277  modsubmod  13285  modsubmodmod  13286  modaddmodup  13290  modmulmod  13292  modsubdir  13296  modfzo0difsn  13299  modsumfzodifsn  13300  uzindi  13338  axdc4uzlem  13339  expneg2  13426  expdiv  13468  expubnd  13529  mulbinom2  13572  bernneq2  13579  expnngt1  13590  hashinfxadd  13734  hashunsngx  13742  hashunsnggt  13743  hashdifsnp1  13842  ccatval3  13921  ccatfv0  13925  ccatval1lsw  13926  ccats1val2  13971  ccatw2s1p1  13983  swrdnd  14004  pfxsuffeqwrdeq  14048  pfxsuff1eqwrdeq  14049  swrdswrd  14055  pfxpfx  14058  wrd2ind  14073  swrdccatin1  14075  pfxccatin12lem1  14078  swrdccatin2  14079  pfxccatin12lem3  14082  swrdccat  14085  pfxccatpfx1  14086  pfxccatpfx2  14087  swrdccat3blem  14089  repswswrd  14134  repswpfx  14135  repswccat  14136  cshwidxmod  14153  2cshw  14163  3cshw  14168  scshwfzeqfzo  14176  cshwcsh2id  14178  cshimadifsn  14179  cshimadifsn0  14180  ccatco  14185  cshco  14186  swrdco  14187  pfxco  14188  lswco  14189  swrds2  14290  2swrd2eqwrdeq  14303  shftuz  14416  abs3dif  14679  fsumdifsnconst  15134  modfsummods  15136  sin02gt0  15533  dvdsval2  15598  dvdscmul  15624  dvdsmulc  15625  dvdscmulr  15626  dvdsmulcr  15627  divalglem8  15739  ndvdssub  15748  rpmulgcd  15894  coprmprod  15993  cncongr1  15999  cncongr2  16000  isprm3  16015  modprm0  16130  coprimeprodsq  16133  pythagtriplem12  16151  pythagtriplem14  16153  pcprendvds  16165  pcmul  16176  pcdiv  16177  pcqcl  16181  pcqdiv  16182  pcdvdsb  16193  vdwnnlem1  16319  hashbcss  16328  cshwshashlem1  16417  fvsetsid  16503  setsstruct2  16509  setsstruct  16511  mrcss  16875  mrcsscl  16879  mrcun  16881  cofulid  17148  catcisolem  17354  funcsetcestrclem9  17401  latleeqj1  17661  lubun  17721  clatleglb  17724  pslem  17804  dirtr  17834  mgmb1mgm1  17853  pwspjmhm  17982  grpinvid1  18092  grpinvid2  18093  grpasscan1  18100  grpasscan2  18101  grpinvadd  18115  grpsubf  18116  grpsubrcan  18118  grpinvsub  18119  grpsubeq0  18123  grpsubadd0sub  18124  grppncan  18128  grpnpcan  18129  mulgnn0p1  18177  mulgaddcomlem  18188  mulginvcom  18190  mulginvinv  18191  subgsubcl  18228  subgsub  18229  eqglact  18269  qussub  18278  ghmsub  18304  psgnunilem4  18554  oddvds2  18622  odsubdvds  18625  gexnnod  18642  slwn0  18669  dvrcl  19365  unitdvcl  19366  dvrcan1  19370  dvrcan3  19371  dvreq1  19372  subrgdv  19481  abvsubtri  19535  idsrngd  19562  lmodvsubval2  19618  lsmcl  19784  lsmsp2  19788  lspsntrim  19799  lidldvgen  19956  ascldimul  20044  mpfsubrg  20244  ply1tmcl  20368  eqcoe1ply1eq  20393  gsummoncoe1  20400  lply1binomsc  20403  chrcong  20604  zndvds  20624  zntoslem  20631  ocvsscon  20747  obselocv  20800  frlmphl  20853  mamudm  20927  mamufacex  20928  scmatf1  21068  scmatf1o  21069  scmatrngiso  21073  submabas  21115  mdetdiaglem  21135  mdetralt2  21146  mdetero  21147  mdetunilem2  21150  mdetunilem6  21154  m2detleiblem7  21164  maducoeval2  21177  gsummatr01lem3  21194  gsummatr01  21196  smadiadetglem2  21209  cramerlem1  21224  mply1topmatcl  21341  mp2pm2mplem4  21345  ntrin  21597  elnei  21647  neindisj2  21659  ordtopn3  21732  leordtval2  21748  lecldbas  21755  cnrest2  21822  cmpsublem  21935  ptrescn  22175  xkococn  22196  kqfeq  22260  snfbas  22402  neifil  22416  fclsrest  22560  utopsnnei  22785  neipcfilu  22832  psmetsym  22847  psmetge0  22849  xmetge0  22881  xmetsym  22884  metustto  23090  metustbl  23103  restmetu  23107  nm2dif  23161  nmtri  23162  cnmet  23307  cnmpopc  23459  iihalf1  23462  iihalf2  23464  iocopnst  23471  clmnegsubdi2  23636  clmsub4  23637  clmvsubval2  23641  ncvspi  23687  cphsqrtcl3  23718  cph2ass  23744  cphipval2  23771  cphipval  23773  caublcls  23839  bcthlem3  23856  bcthlem4  23857  srabn  23890  cssbn  23905  cmslsschl  23907  rrxmet  23938  rrxdsfi  23941  iblconst  24345  tdeglem3  24580  mdegmullem  24599  dvdsq1p  24681  coeid3  24757  aannenlem2  24845  pserdvlem2  24943  tanord1  25048  cxpef  25175  recxpcl  25185  logbchbase  25276  relogbcl  25278  relogbzcl  25279  logbleb  25288  logblt  25289  relogbcxpb  25292  lawcos  25321  pythag  25322  isosctrlem1  25323  isosctrlem2  25324  lgsmodeq  25845  lgsmulsqcoprm  25846  gausslemma2dlem1a  25868  2lgsoddprmlem2  25912  ax5seglem1  26641  axcontlem2  26678  axcontlem8  26684  upgrpredgv  26851  numedglnl  26856  issubgr2  26981  uhgrissubgr  26984  egrsubgr  26986  nbusgrfi  27083  nb3grprlem2  27090  cplgr3v  27144  cusgrsizeindslem  27160  finsumvtxdg2size  27259  rusgrpropadjvtx  27294  upgrwlkvtxedg  27353  usgr2trlncl  27468  uspgrn2crct  27513  crctcshwlkn0lem4  27518  crctcshwlkn0lem5  27519  wwlksnextproplem3  27617  umgr2adedgwlklem  27650  rusgr0edg  27679  clwwlk1loop  27693  clwwlkccatlem  27694  clwlkclwwlklem2a4  27702  clwlkclwwlklem2a  27703  clwwisshclwwslemlem  27718  erclwwlktr  27727  clwwlkel  27752  erclwwlkntr  27777  clwwlknonex2lem2  27814  uhgr3cyclex  27888  umgr3cyclex  27889  eucrctshift  27949  frgr3v  27981  3cyclfrgrrn  27992  frgrwopreglem5a  28017  frgr2wsp1  28036  extwwlkfab  28058  clwwlknonclwlknonf1o  28068  numclwwlk3lem1  28088  numclwwlk5  28094  numclwwlk6  28096  isgrpo  28201  grpoinvid1  28232  grpoinvid2  28233  grpoinvop  28237  grpodivinv  28240  grpoinvdiv  28241  grpodivf  28242  grponpcan  28247  ablonncan  28260  nvmval  28346  nvmval2  28347  nvmfval  28348  nvmul0or  28354  nvpncan2  28357  nvaddsub4  28361  nvmeq0  28362  nvdif  28370  nvpi  28371  nvmtri  28375  nvabs  28376  imsmetlem  28394  ipval2lem3  28409  ipval2  28411  4ipval2  28412  ipval3  28413  nmooge0  28471  blometi  28507  hvaddsub12  28742  hvsubdistr1  28753  hvsubdistr2  28754  hvaddcan2  28775  hvmulcan  28776  hvmulcan2  28777  hvsubcan  28778  hvsubcan2  28779  his7  28794  his2sub  28796  his2sub2  28797  norm3dif2  28855  shsubcl  28924  hhssnv  28968  shlej2  29065  fh2  29323  cm2j  29324  pjoi0  29421  hodcl  29451  hosubdi  29512  unopf1o  29620  unopadj  29623  adj2  29638  braadd  29649  bramul  29650  lnopaddmuli  29677  lnopsubmuli  29679  homco2  29681  lnfnaddmuli  29749  adjlnop  29790  leopmul  29838  leoptr  29841  pjimai  29880  atcv1  30084  atexch  30085  atcvatlem  30089  fcoinvbr  30286  divnumden2  30460  xdivmul  30528  cshf1o  30563  dvdschrmulg  30785  resvsca  30830  hasheuni  31243  difelsiga  31291  cndprobin  31591  bayesth  31596  sgn3da  31698  signstfvp  31740  breprexplemc  31802  hashfundm  32251  hashf1dmcdm  32253  swrdrevpfx  32260  swrdwlk  32270  lediv2aALT  32817  fununiq  32909  dfrdg2  32937  sltres  33066  sletr  33134  clsun  33573  neiin  33577  rdgeqoa  34533  curfv  34753  matunitlindflem1  34769  poimirlem32  34805  ftc1anclem4  34851  areacirc  34868  filbcmb  34896  ismtybnd  34966  grpoeqdivid  35040  ghomco  35050  rngonegrmul  35103  zerdivemp1x  35106  rngohomco  35133  rngoisoco  35141  riscer  35147  intidl  35188  isfldidl  35227  brredunds  35741  lshpnelb  36000  opnlen0  36204  opcon3b  36212  opcon2b  36213  oplecon3b  36216  opltcon3b  36220  opltcon2b  36222  oldmm1  36233  oldmm4  36236  oldmj1  36237  oldmj4  36240  cvrval2  36290  cvrcon3b  36293  leatb  36308  atcmp  36327  atcvreq0  36330  atlatle  36336  athgt  36472  3dim2  36484  islln2a  36533  lplnnleat  36558  lvolnleat  36599  4atlem10  36622  4atlem11  36625  4atlem12  36628  dalem21  36710  dalem22  36711  dalem23  36712  dalem29  36717  dalem30  36718  dalem31N  36719  dalem32  36720  dalem33  36721  dalem34  36722  dalem35  36723  dalem36  36724  dalem37  36725  dalem40  36728  dalem46  36734  dalem47  36735  dalem51  36739  dalem52  36740  dalem58  36746  dalem59  36747  pmaple  36777  paddclN  36858  pmapjoin  36868  pmapjat1  36869  elpcliN  36909  pclssN  36910  pclun2N  36915  2polcon4bN  36934  paddunN  36943  poldmj1N  36944  pmapj2N  36945  pmapocjN  36946  psubclinN  36964  paddatclN  36965  poml4N  36969  lautco  37113  ldilco  37132  ltrneq2  37164  trljat1  37182  cdlemc1  37207  cdleme10  37270  ltrnco  37735  trlcocnv  37736  trljco  37756  trljco2  37757  cdlemi1  37834  tendocnv  38037  diaord  38063  dibord  38175  dihord3  38273  dihord4  38274  dihmeetlem2N  38315  dihmeetlem4preN  38322  dochdmj1  38406  hdmap10lem  38855  dvdsexpim  39059  expgcd  39061  zexpgcd  39063  readdsub  39092  reltsub1  39094  renpncan3  39099  reppncan  39101  resubdi  39104  readdcan2  39120  mzprename  39224  dvdsrabdioph  39285  pell14qrdivcl  39340  monotoddzz  39418  jm2.19lem2  39465  jm2.19  39468  relexpaddss  39941  k0004lem3  40377  dvconstbi  40543  chordthmALT  41144  isosctrlem1ALT  41145  ssinc  41230  ssdec  41231  wessf1ornlem  41321  disjf1o  41328  disjinfi  41330  ssnnf1octb  41332  projf1o  41335  mapssbi  41352  iunmapsn  41356  upbdrech  41448  iuneqfzuzlem  41478  suplesup  41483  rexabslelem  41568  climxrrelem  41906  limsupresxr  41923  liminfresxr  41924  liminfvalxr  41940  xlimliminflimsup  42019  cncfshift  42033  cncfperiod  42038  cncfuni  42045  icccncfext  42046  dvmptfprodlem  42105  dvnprodlem1  42107  itgspltprt  42140  ismbl3  42148  stoweidlem3  42165  stoweidlem10  42172  stoweidlem19  42181  stoweidlem31  42193  stoweidlem34  42196  stoweidlem44  42206  fourierdlem41  42310  fourierdlem42  42311  fourierdlem51  42319  fourierdlem68  42336  fourierdlem89  42357  fourierdlem91  42359  fourierdlem92  42360  fourierdlem94  42362  etransclem24  42420  etransclem34  42430  qndenserrnbllem  42456  salincl  42485  saldifcl2  42488  subsalsal  42519  sge0pr  42553  sge0pnffigt  42555  sge0reuz  42606  nnfoctbdjlem  42614  nnfoctbdj  42615  meadjiunlem  42624  caratheodorylem2  42686  hoidmv1le  42753  hoidmvlelem3  42756  hspmbllem2  42786  opnvonmbllem2  42792  sssmf  42892  smfaddlem1  42916  sigaraf  42987  sigarmf  42988  nltle2tri  43390  subsubelfzo0  43403  iccpartiltu  43459  icceuelpart  43473  poprelb  43563  reuopreuprim  43565  proththd  43656  mogoldbblem  43762  fppr2odd  43773  fpprel2  43783  bgoldbtbndlem2  43848  isomgrtr  43881  nn0sumltlt  44326  invginvrid  44343  ply1sclrmsm  44365  linccl  44397  lincvalpr  44401  lincresunit3lem1  44462  lincresunit3  44464  fdivmpt  44528  nnolog2flm1  44578  dignnld  44591  digexp  44595  dignn0flhalflem1  44603  reorelicc  44625  eenglngeehlnmlem1  44652  line2  44667  line2xlem  44668  itsclc0lem1  44671  itsclc0xyqsolr  44684  setrec2fun  44723  reccot  44785  rectan  44786
  Copyright terms: Public domain W3C validator