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

Theorem anim12i 587
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 492 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382
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
This theorem is referenced by:  anim12ci  588  anim1i  589  anim2i  590  anifp  1013  sbimi  1872  cgsex2g  3211  cgsex4g  3212  spc2egv  3267  sseq2  3589  uneqin  3836  undif3OLD  3847  disjpr2  4193  ssunieq  4402  iuneq1  4464  iuneq2  4467  copsex2t  4876  soeq2  4968  opbrop  5110  xpsspw  5144  coeq1  5188  coeq2  5189  cnveq  5205  dmeq  5232  sotri  5428  tz7.7  5651  funun  5831  fununfun  5833  fundif  5834  funprg  5839  funtp  5844  funcnvqpOLD  5852  2elresin  5901  funssxp  5959  fssres  5967  f1co  6007  foun  6052  resdif  6054  f1oco  6056  fvun  6162  elfvmptrab1  6197  fvn0ssdmfun  6242  dff3  6264  exfo  6269  fprg  6304  ftpg  6305  weisoeq2  6483  oprabv  6578  ndmovdistr  6698  ndmovord  6699  brrpssg  6814  eldifpw  6845  iunpw  6847  bropfvvvv  7121  f1o2ndf1  7149  fvn0elsupp  7175  wfrlem5  7283  smores  7313  tz7.49  7404  tz7.49c  7405  oaord  7491  oeeulem  7545  nnaord  7563  brecop  7704  brecop2  7705  eroveu  7706  ecopovtrn  7714  ixpeq2  7785  undifixp  7807  undom  7910  sbthlem8  7939  sbthlem9  7940  unxpdom  8029  isinf  8035  f1opwfi  8130  fiin  8188  en2lp  8370  inf3lem3  8387  tcmin  8477  alephfp  8791  kmlem16  8847  cdaval  8852  cdaun  8854  cofsmo  8951  fin23lem28  9022  axdc3lem2  9133  ac6c4  9163  brdom3  9208  brdom5  9209  brdom4  9210  canthp1lem2  9331  finngch  9333  ordpipq  9620  adderpq  9634  mulerpq  9635  lterpq  9648  genpn0  9681  genpnnp  9683  addclprlem2  9695  addcmpblnr  9746  addsrpr  9752  mulsrpr  9753  addclsr  9760  addasssr  9765  distrsr  9768  0idsr  9774  1idsr  9775  00sr  9776  mulgt0sr  9782  axaddf  9822  axaddass  9833  axdistr  9835  cnegex  10068  recextlem2  10509  difgtsumgt  11195  zaddcl  11252  qaddcl  11638  qmulcl  11640  qreccl  11642  xmulgt0  11944  xrsupsslem  11967  xrinfmsslem  11968  supxrpnf  11978  iccss  12070  difreicc  12133  fzadd2  12204  fzsubel  12205  ssfzunsn  12214  elfz0add  12264  difelfznle  12279  2ffzeq  12286  nelfzo  12301  fzonmapblen  12338  ubmelfzo  12357  ubmelm1fzo  12387  elfznelfzo  12396  subfzo0  12409  adddivflid  12438  modifeq2int  12551  modaddmodup  12552  addmodlteq  12564  fsuppmapnn0fiub  12609  fsuppmapnn0fiubOLD  12610  mulexp  12718  mulexpz  12719  leexp1a  12738  faclbnd  12896  hashunx  12990  wrdeq  13130  ccatcl  13160  swrdnd  13232  swrdeq  13244  swrdsbslen  13248  swrdspsleq  13249  swrdswrdlem  13259  reuccats1  13280  swrdccatin12lem2a  13284  swrdccatin2  13286  swrdccatin12lem2  13288  swrdccatin12  13290  swrdccat  13292  repswswrd  13330  repswccat  13331  cshwidxn  13354  cshweqdif2  13364  2cshwcshw  13370  cshwcshid  13372  cshwcsh2id  13373  f1oun2prg  13460  s2eq2s1eq  13479  wwlktovf1  13496  s3sndisj  13502  s3iunsndisj  13503  sqabsadd  13818  sqabssub  13819  abs2dif  13868  rexanuz  13881  o1of2  14139  o1rlimmul  14145  fsum2dlem  14291  isumltss  14367  fprodser  14466  fprodeq0  14492  fprod2dlem  14497  dvdscmulr  14796  dvdsmulcr  14797  summodnegmod  14798  dvds2ln  14800  dvdsflip  14825  divalglem9  14910  gcdcllem3  15009  gcdaddmlem  15031  gcdabs  15036  sqgcd  15064  lcmcllem  15095  lcmabs  15104  lcmgcdlem  15105  lcmgcd  15106  lcmgcdeq  15111  lcmf  15132  lcmftp  15135  lcmfunsnlem2lem1  15137  qredeq  15157  cncongr1  15167  cncongr2  15168  isprm7  15206  divgcdodd  15208  hashgcdlem  15279  pythagtriplem19  15324  dvdsprmpweqle  15376  difsqpwdvds  15377  prmgaplem4  15544  cshwsidrepsw  15586  setsfun0  15674  setsstruct  15675  xpsfrnel2  15996  isfunc  16295  fpwipodrs  16935  tsrss  16994  resmhm2  17131  gimco  17481  symg2bas  17589  pgrpsubgsymg  17599  symgextf  17608  gsmsymgrfixlem1  17618  fvcosymgeq  17620  gsmsymgreqlem1  17621  symgfixf1  17628  efgrelexlema  17933  gsum2dlem1  18140  gsum2dlem2  18141  dvdsr  18417  subrgpropd  18585  islmhm2  18807  ressmpladd  19226  ressmplmul  19227  mplind  19271  psgnghm  19692  psgndiflemB  19712  frlmbas3  19881  frlmphl  19886  islindf4  19943  mpt2matmul  20018  mavmul0g  20125  1marepvsma1  20155  mdetdiag  20171  slesolvec  20251  cramerimplem2  20256  cramerimplem3  20257  cramerimp  20258  mat2pmatlin  20306  m2pmfzgsumcl  20319  monmatcollpw  20350  pmatcollpw3lem  20354  pmatcollpwscmatlem1  20360  chpmat1dlem  20406  chfacfisf  20425  chfacfisfcpmat  20426  chfacfpmmulgsum2  20436  tgcl  20531  uncld  20602  innei  20686  cnco  20827  uncmp  20963  txbas  21127  txbasval  21166  tx1stc  21210  fbun  21401  infil  21424  fbunfip  21430  filuni  21446  imaelfm  21512  txflf  21567  tsmsfbas  21688  tsmsxp  21715  blin2  21991  nmhmplusg  22318  qtopbaslem  22319  iccntr  22379  ncvspi  22708  ncvs1  22709  unmbl  23056  volfiniun  23066  mbfi1flimlem  23239  ply1idom  23632  logreclem  24244  relogbcxpb  24269  fsumvma2  24683  chpchtsum  24688  dchrelbas3  24707  dchrmulcl  24718  lgsmulsqcoprm  24812  gausslemma2dlem1a  24834  lgsquad2lem2  24854  dchrisum0fmul  24939  dchrisum0lem1  24949  ishpg  25396  brcgr  25525  brbtwn2  25530  axcontlem2  25590  usgraidx2v  25715  nb3gra2nb  25777  sizeusglecusg  25807  redwlk  25929  wlkdvspthlem  25930  usgra2adedgwlkon  25936  usgra2wlkspthlem1  25940  constr3lem6  25970  constr3trllem2  25972  cusconngra  25997  2wlkeq  26028  usg2wlkeq2  26030  wwlkextinj  26051  clwlkisclwwlklem2a  26106  clwlkisclwwlklem0  26109  clwwisshclww  26128  clwlkf1clwwlk  26170  el2wlkonotot0  26192  usg2spthonot0  26209  rusgranumwlkl1  26267  rusgra0edg  26275  iseupa  26285  frgra3v  26322  1to3vfriswmgra  26327  4cycl2v2nb  26336  frgranbnb  26340  frgrawopreg  26369  frg2woteqm  26379  2spotiundisj  26382  frghash2spot  26383  usg2spot2nb  26385  extwwlkfablem2  26398  numclwwlkovgelim  26409  numclwlk1lem2fo  26415  numclwwlk2  26427  frgrareggt1  26436  blocni  26837  hvsub4  27071  shscli  27353  shscom  27355  spanunsni  27615  spanpr  27616  5oalem2  27691  5oalem3  27692  5oalem5  27694  3oalem1  27698  hoscl  27781  hoadddi  27839  hoadddir  27840  hosub4  27849  lnophsi  28037  hmops  28056  hmopm  28057  adjadd  28129  leop2  28160  leopadd  28168  leopmuli  28169  pjclem4  28235  pj3si  28243  mdslmd1lem2  28362  mdslmd3i  28368  atomli  28418  atcvatlem  28421  chirredlem3  28428  chirredi  28430  atcvat3i  28432  mdsymlem1  28439  mdsymlem5  28443  cdjreui  28468  cdj3i  28477  addltmulALT  28482  spc2ed  28489  mndpluscn  29093  sxbrsigalem5  29470  probfinmeasbOLD  29610  bnj545  30012  bnj546  30013  bnj557  30018  bnj570  30022  bnj594  30029  bnj1001  30075  bnj1118  30099  txpcon  30261  cvmlift2lem10  30341  lediv2aALT  30618  poseq  30787  frrlem5  30821  sltres  30854  nocvxminlem  30882  altopeq12  31032  altxpsspw  31047  funtransport  31101  neibastop1  31317  filnetlem3  31338  lukshef-ax2  31377  arg-ax  31378  nndivsub  31419  isbasisrelowllem1  32162  isbasisrelowllem2  32163  icoreclin  32164  relowlssretop  32170  rdgeqoa  32177  wl-ax11-lem2  32325  matunitlindflem1  32358  matunitlindflem2  32359  poimirlem4  32366  poimirlem26  32388  poimirlem29  32391  poimirlem30  32392  heicant  32397  mblfinlem1  32399  ismblfin  32403  itg2addnclem  32414  ftc1anclem6  32443  ftc1anclem7  32444  ftc1anclem8  32445  ftc1anc  32446  prdstotbnd  32546  heibor1lem  32561  isdrngo2  32710  divrngidl  32780  pridlc3  32825  linepsubN  33839  pmapsub  33855  elpaddri  33889  paddasslem14  33920  pmapjoin  33939  dvhfvadd  35181  dvhvaddcomN  35186  rmxynorm  36284  monotoddzzfi  36308  acongtr  36346  mpaaeu  36522  brfvrcld2  36786  rfovcnvf1od  37101  nzin  37322  pm10.14  37363  etransclem38  38948  2reu4a  39621  2reu4  39622  icceuelpartlem  39757  icceuelpart  39758  sqrtpwpw2p  39772  fmtnoprmfac1lem  39798  fmtnoprmfac1  39799  lighneallem2  39845  divgcdoddALTV  39915  gbopos  39965  gbogt5  39968  gboage9  39970  nnsum3primesgbe  39992  bgoldbtbndlem2  40006  bgoldbtbndlem3  40007  pfxeq  40051  pfxsuffeqwrdeq  40053  pfxccat1  40057  pfxccatin12lem2  40071  pfxccatin12  40072  propeqop  40105  iunopeqop  40110  2elfz2melfz  40161  fz0addge0  40162  2ffzoeq  40167  uhgruhgra  40273  uspgredg2v  40432  usgredg2v  40435  usgr2v1e2w  40459  nb3gr2nb  40593  cusgredg  40627  cplgr3v  40638  cusgrop  40641  rusgr1vtx  40769  is1wlkg  40797  1wlkeq  40819  1wlk1walk  40824  uspgr2wlkeq2  40836  uspgr2wlkeqi  40837  usgr2wlkneq  40943  usgr2pth  40951  crctcsh1wlkn0lem3  40996  crctcsh1wlkn0lem4  40997  crctcsh1wlkn0lem5  40998  wspthneq1eq2  41037  wlkwwlkfun  41073  wwlksnextinj  41086  21wlkdlem7  41120  21wlkdlem8  41121  2pthon3v-av  41131  s3wwlks2on  41141  elwwlks2  41151  elwspths2spth  41152  rusgrnumwwlks  41158  clwwlknp  41176  clwlkclwwlklem2a  41188  clwlkclwwlklem3  41191  clwlksf1clwwlk  41257  31wlkdlem3  41309  uhgr3cyclex  41330  cusconngr  41339  eupth0  41363  frgr3v  41426  1to3vfriswmgr  41431  4cycl2v2nb-av  41440  frgrnbnb  41444  frgrncvvdeq  41461  frgrwopreg  41467  frgrhash2wsp  41478  av-numclwlk1lem2fo  41506  av-numclwwlk2lem1  41513  av-numclwwlk2  41518  rabsubmgmd  41562  resmgmhm2  41570  ismhm0  41576  mhmismgmhm  41577  isrnghmmul  41664  c0ghm  41682  rhmisrnghm  41691  rnghmsubcsetclem2  41749  rngcinv  41754  rngcinvALTV  41766  rhmsubcsetclem2  41795  rhmsubcrngclem2  41801  ringcinv  41805  ringcinvALTV  41829  srhmsubc  41849  srhmsubcALTV  41868  mapprop  41898  zlmodzxzadd  41910  domnmsuppn0  41925  mndpfsupp  41932  ply1mulgsumlem2  41950  lincsum  41993  lincsumcl  41995  lincscmcl  41996  isldepslvec2  42049  modn0mul  42090  digexp  42180
  Copyright terms: Public domain W3C validator