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

Theorem anim12i 589
Description: Conjoin antecedents and consequents of two premises. (Contributed by NM, 3-Jan-1993.) (Proof shortened by Wolf Lammen, 14-Dec-2013.)
Hypotheses
Ref Expression
anim12i.1 (𝜑𝜓)
anim12i.2 (𝜒𝜃)
Assertion
Ref Expression
anim12i ((𝜑𝜒) → (𝜓𝜃))

Proof of Theorem anim12i
StepHypRef Expression
1 anim12i.1 . 2 (𝜑𝜓)
2 anim12i.2 . 2 (𝜒𝜃)
3 id 22 . 2 ((𝜓𝜃) → (𝜓𝜃))
41, 2, 3syl2an 493 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383
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
This theorem is referenced by:  anim12ci  590  anim1i  591  anim2i  592  anifp  1040  sbimi  1943  cgsex2g  3270  cgsex4g  3271  spc2egv  3326  sseq2  3660  uneqin  3911  undif3OLD  3922  disjpr2  4280  ssunieq  4504  iuneq1  4566  iuneq2  4569  copsex2t  4986  propeqop  4999  iunopeqop  5010  soeq2  5084  opbrop  5232  xpsspw  5266  coeq1  5312  coeq2  5313  cnveq  5328  dmeq  5356  sotri  5558  tz7.7  5787  funun  5970  fununfun  5972  fundif  5973  funprg  5978  funtp  5983  funcnvqpOLD  5991  2elresin  6040  funssxp  6099  fssres  6108  f1co  6148  foun  6193  resdif  6195  f1oco  6197  fvun  6307  elfvmptrab1  6344  fvn0ssdmfun  6390  dff3  6412  exfo  6417  fprg  6462  ftpg  6463  weisoeq2  6646  oprabv  6745  ndmovdistr  6865  ndmovord  6866  brrpssg  6981  eldifpw  7018  iunpw  7020  bropfvvvv  7302  f1o2ndf1  7330  fvn0elsupp  7356  wfrlem5  7464  smores  7494  tz7.49  7585  tz7.49c  7586  oaord  7672  oeeulem  7726  nnaord  7744  brecop  7883  brecop2  7884  eroveu  7885  ecopovtrn  7893  ixpeq2  7964  undifixp  7986  undom  8089  sbthlem8  8118  sbthlem9  8119  unxpdom  8208  isinf  8214  f1opwfi  8311  fiin  8369  en2lp  8548  inf3lem3  8565  tcmin  8655  alephfp  8969  kmlem16  9025  cdaval  9030  cdaun  9032  cofsmo  9129  fin23lem28  9200  axdc3lem2  9311  ac6c4  9341  brdom3  9388  brdom5  9389  brdom4  9390  canthp1lem2  9513  finngch  9515  ordpipq  9802  adderpq  9816  mulerpq  9817  lterpq  9830  genpn0  9863  genpnnp  9865  addclprlem2  9877  addcmpblnr  9928  addsrpr  9934  mulsrpr  9935  addclsr  9942  addasssr  9947  distrsr  9950  0idsr  9956  1idsr  9957  00sr  9958  mulgt0sr  9964  axaddf  10004  axaddass  10015  axdistr  10017  cnegex  10255  recextlem2  10696  difgtsumgt  11384  zaddcl  11455  qaddcl  11842  qmulcl  11844  qreccl  11846  xmulgt0  12151  xrsupsslem  12175  xrinfmsslem  12176  supxrpnf  12186  iccss  12279  difreicc  12342  fzadd2  12414  fzsubel  12415  ssfzunsnext  12424  elfz0add  12477  difelfznle  12492  2ffzeq  12499  nelfzo  12514  fzonmapblen  12553  ubmelfzo  12572  ubmelm1fzo  12604  elfznelfzo  12613  subfzo0  12630  adddivflid  12659  modifeq2int  12772  modaddmodup  12773  addmodlteq  12785  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  mulexp  12939  mulexpz  12940  leexp1a  12959  faclbnd  13117  hashunx  13213  wrdeq  13359  ccatcl  13392  swrdnd  13478  swrdeq  13490  swrdsbslen  13494  swrdspsleq  13495  swrdswrdlem  13505  reuccats1  13526  swrdccatin12lem2a  13531  swrdccatin2  13533  swrdccatin12lem2  13535  swrdccatin12  13537  swrdccat  13539  repswswrd  13577  repswccat  13578  cshwidxn  13601  cshweqdif2  13611  2cshwcshw  13617  cshwcshid  13619  cshwcsh2id  13620  f1oun2prg  13708  s2eq2s1eq  13727  s3eqs2s1eq  13729  wwlktovf1  13746  s3sndisj  13752  s3iunsndisj  13753  sqabsadd  14066  sqabssub  14067  abs2dif  14116  rexanuz  14129  o1of2  14387  o1rlimmul  14393  fsum2dlem  14545  isumltss  14624  fprodser  14723  fprodeq0  14749  fprod2dlem  14754  dvdscmulr  15057  dvdsmulcr  15058  summodnegmod  15059  dvds2ln  15061  dvdsflip  15086  divalglem9  15171  gcdcllem3  15270  gcdaddmlem  15292  gcdabs  15297  sqgcd  15325  lcmcllem  15356  lcmabs  15365  lcmgcdlem  15366  lcmgcd  15367  lcmgcdeq  15372  lcmf  15393  lcmftp  15396  lcmfunsnlem2lem1  15398  qredeq  15418  cncongr1  15428  cncongr2  15429  isprm7  15467  hashgcdlem  15540  pythagtriplem19  15585  dvdsprmpweqle  15637  difsqpwdvds  15638  prmgaplem4  15805  cshwsidrepsw  15847  setsfun0  15941  setsstruct2  15943  setsstructOLD  15946  xpsfrnel2  16272  isfunc  16571  fpwipodrs  17211  tsrss  17270  resmhm2  17407  gimco  17757  symg2bas  17864  pgrpsubgsymg  17874  symgextf  17883  gsmsymgrfixlem1  17893  fvcosymgeq  17895  gsmsymgreqlem1  17896  symgfixf1  17903  efgrelexlema  18208  gsum2dlem1  18415  gsum2dlem2  18416  dvdsr  18692  subrgpropd  18862  islmhm2  19086  ressmpladd  19505  ressmplmul  19506  mplind  19550  psgnghm  19974  psgndiflemB  19994  frlmbas3  20163  frlmphl  20168  islindf4  20225  mpt2matmul  20300  mavmul0g  20407  1marepvsma1  20437  mdetdiag  20453  slesolvec  20533  cramerimplem2  20538  cramerimplem3  20539  cramerimp  20540  mat2pmatlin  20588  m2pmfzgsumcl  20601  monmatcollpw  20632  pmatcollpw3lem  20636  pmatcollpwscmatlem1  20642  chpmat1dlem  20688  chfacfisf  20707  chfacfisfcpmat  20708  chfacfpmmulgsum2  20718  tgcl  20821  uncld  20893  innei  20977  cnco  21118  uncmp  21254  txbas  21418  txbasval  21457  tx1stc  21501  fbun  21691  infil  21714  fbunfip  21720  filuni  21736  imaelfm  21802  txflf  21857  tsmsfbas  21978  tsmsxp  22005  blin2  22281  nmhmplusg  22608  qtopbaslem  22609  iccntr  22671  ncvspi  23002  ncvs1  23003  unmbl  23351  volfiniun  23361  mbfi1flimlem  23534  ply1idom  23929  logreclem  24545  relogbcxpb  24570  fsumvma2  24984  chpchtsum  24989  dchrelbas3  25008  dchrmulcl  25019  lgsmulsqcoprm  25113  gausslemma2dlem1a  25135  lgsquad2lem2  25155  dchrisum0fmul  25240  dchrisum0lem1  25250  ishpg  25696  brcgr  25825  brbtwn2  25830  axcontlem2  25890  uspgredg2v  26161  usgredg2v  26164  usgr2v1e2w  26189  nb3gr2nb  26330  cusgredg  26376  cplgr3v  26387  cusgrop  26390  rusgr1vtx  26540  iswlkg  26565  wlkeq  26585  wlk1walk  26591  uspgr2wlkeq2  26599  uspgr2wlkeqi  26600  crctcshwlkn0lem3  26760  crctcshwlkn0lem4  26761  crctcshwlkn0lem5  26762  wspthneq1eq2  26814  wlkwwlkfun  26849  wwlksnextinj  26862  2wlkdlem7  26897  2wlkdlem8  26898  2pthon3v  26908  s3wwlks2on  26922  elwwlks2  26933  elwspths2spth  26934  rusgrnumwwlks  26941  clwlkclwwlklem2a  26964  clwlkclwwlklem3  26967  clwlksf1clwwlk  27056  clwwlknonex2  27084  3wlkdlem3  27139  uhgr3cyclex  27160  cusconngr  27169  eupth0  27192  frgr3v  27255  1to3vfriswmgr  27260  4cycl2v2nb  27269  frgrnbnb  27273  frgrncvvdeq  27289  frgrwopreglem4a  27290  frgrwopreglem5a  27291  frgrwopreglem4  27295  frgrwopreglem5  27301  frgrhash2wsp  27312  clwwlkccatlem  27331  numclwlk1lem2foa  27344  numclwwlk2  27361  numclwwlk2OLD  27368  blocni  27788  hvsub4  28022  shscli  28304  shscom  28306  spanunsni  28566  spanpr  28567  5oalem2  28642  5oalem3  28643  5oalem5  28645  3oalem1  28649  hoscl  28732  hoadddi  28790  hoadddir  28791  hosub4  28800  lnophsi  28988  hmops  29007  hmopm  29008  adjadd  29080  leop2  29111  leopadd  29119  leopmuli  29120  pjclem4  29186  pj3si  29194  mdslmd1lem2  29313  mdslmd3i  29319  atomli  29369  atcvatlem  29372  chirredlem3  29379  chirredi  29381  atcvat3i  29383  mdsymlem1  29390  mdsymlem5  29394  cdjreui  29419  cdj3i  29428  addltmulALT  29433  spc2ed  29440  mndpluscn  30100  sxbrsigalem5  30478  probfinmeasbOLD  30618  bnj545  31091  bnj546  31092  bnj557  31097  bnj570  31101  bnj594  31108  bnj1001  31154  bnj1118  31178  txpconn  31340  cvmlift2lem10  31420  lediv2aALT  31697  poseq  31878  frrlem5  31909  sltres  31940  nocvxminlem  32018  sslttr  32039  altopeq12  32194  altxpsspw  32209  funtransport  32263  neibastop1  32479  filnetlem3  32500  lukshef-ax2  32539  arg-ax  32540  nndivsub  32581  isbasisrelowllem1  33333  isbasisrelowllem2  33334  icoreclin  33335  relowlssretop  33341  rdgeqoa  33348  wl-ax11-lem2  33493  matunitlindflem1  33535  matunitlindflem2  33536  poimirlem4  33543  poimirlem26  33565  poimirlem29  33568  poimirlem30  33569  heicant  33574  mblfinlem1  33576  ismblfin  33580  itg2addnclem  33591  ftc1anclem6  33620  ftc1anclem7  33621  ftc1anclem8  33622  ftc1anc  33623  prdstotbnd  33723  heibor1lem  33738  isdrngo2  33887  divrngidl  33957  pridlc3  34002  linepsubN  35356  pmapsub  35372  elpaddri  35406  paddasslem14  35437  pmapjoin  35456  dvhfvadd  36697  dvhvaddcomN  36702  rmxynorm  37800  monotoddzzfi  37824  acongtr  37862  mpaaeu  38037  brfvrcld2  38301  rfovcnvf1od  38615  nzin  38834  pm10.14  38875  liminfvalxr  40333  etransclem38  40807  2reu4a  41510  2reu4  41511  2elfz2melfz  41653  fz0addge0  41654  2ffzoeq  41663  icceuelpartlem  41696  icceuelpart  41697  pfxeq  41729  pfxsuffeqwrdeq  41731  pfxccat1  41735  pfxccatin12lem2  41749  pfxccatin12  41750  sqrtpwpw2p  41775  fmtnoprmfac1lem  41801  fmtnoprmfac1  41802  lighneallem2  41848  divgcdoddALTV  41918  gbowpos  41972  gbowgt5  41975  gboge9  41977  nnsum3primesgbe  42005  bgoldbtbndlem2  42019  bgoldbtbndlem3  42020  isupwlkg  42043  rabsubmgmd  42116  resmgmhm2  42124  ismhm0  42130  mhmismgmhm  42131  isrnghmmul  42218  c0ghm  42236  rhmisrnghm  42245  rnghmsubcsetclem2  42301  rngcinv  42306  rngcinvALTV  42318  rhmsubcsetclem2  42347  rhmsubcrngclem2  42353  ringcinv  42357  ringcinvALTV  42381  srhmsubc  42401  srhmsubcALTV  42419  mapprop  42449  zlmodzxzadd  42461  domnmsuppn0  42475  mndpfsupp  42482  ply1mulgsumlem2  42500  lincsum  42543  lincsumcl  42545  lincscmcl  42546  isldepslvec2  42599  modn0mul  42640  digexp  42726
  Copyright terms: Public domain W3C validator