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

Theorem anim12i 602
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 585 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 384
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 198  df-an 385
This theorem is referenced by:  anim12ci  603  anim1i  604  anim2i  605  anifp  1086  sbimi  2067  cgsex2g  3444  cgsex4g  3445  spc2egv  3499  sseq2  3835  uneqin  4091  disjpr2  4451  ssunieq  4677  iuneq1  4737  iuneq2  4740  copsex2t  5159  propeqop  5175  opthhausdorff  5185  opthhausdorff0  5186  iunopeqop  5189  soeq2  5265  opbrop  5413  xpsspw  5447  coeq1  5494  coeq2  5495  cnveq  5510  dmeq  5538  sotri  5747  tz7.7  5975  funun  6155  fununfun  6157  fundif  6158  funprg  6163  funtp  6166  2elresin  6222  funssxp  6285  fssres  6294  f1co  6335  foun  6380  resdif  6382  f1oco  6384  fvun  6498  elfvmptrab1  6535  fvn0ssdmfun  6581  dff3  6603  exfo  6608  fprg  6655  ftpg  6656  weisoeq2  6839  oprabv  6942  ndmovdistr  7062  ndmovord  7063  brrpssg  7178  eldifpw  7215  iunpw  7217  bropfvvvv  7500  f1o2ndf1  7528  fvn0elsupp  7554  wfrlem5  7664  smores  7694  tz7.49  7785  tz7.49c  7786  oaord  7873  oeeulem  7927  nnaord  7945  brecop  8084  brecop2  8085  brecop2OLD  8086  eroveu  8087  ecopovtrn  8095  ixpeq2  8168  undifixp  8190  undom  8296  sbthlem8  8325  sbthlem9  8326  unxpdom  8415  isinf  8421  f1opwfi  8518  fiin  8576  en2lp  8758  inf3lem3  8783  tcmin  8873  alephfp  9223  kmlem16  9281  cdaval  9286  cdaun  9288  cofsmo  9385  fin23lem28  9456  axdc3lem2  9567  ac6c4  9597  brdom3  9644  brdom5  9645  brdom4  9646  canthp1lem2  9769  finngch  9771  ordpipq  10058  adderpq  10072  mulerpq  10073  lterpq  10086  genpn0  10119  genpnnp  10121  addclprlem2  10133  addcmpblnr  10184  addsrpr  10190  mulsrpr  10191  addclsr  10198  addasssr  10203  distrsr  10206  0idsr  10212  1idsr  10213  00sr  10214  mulgt0sr  10220  axaddf  10260  axaddass  10271  axdistr  10273  cnegex  10511  recextlem2  10952  difgtsumgt  11631  zaddcl  11702  qaddcl  12042  qmulcl  12044  qreccl  12046  xmulgt0  12350  xrsupsslem  12374  xrinfmsslem  12375  supxrpnf  12385  iccss  12478  difreicc  12546  fzadd2  12618  fzsubel  12619  ssfzunsnext  12628  elfz0add  12681  difelfznle  12696  2ffzeq  12703  nelfzo  12718  fzonmapblen  12757  ubmelfzo  12776  ubmelm1fzo  12807  elfznelfzo  12816  subfzo0  12833  adddivflid  12862  modifeq2int  12975  modaddmodup  12976  addmodlteq  12988  fsuppmapnn0fiub  13033  mulexp  13141  mulexpz  13142  leexp1a  13161  faclbnd  13316  hashunx  13412  wrdeq  13557  ccatcl  13590  swrdnd  13675  swrdeq  13687  swrdsbslen  13691  swrdspsleq  13692  swrdswrdlem  13702  reuccats1  13723  swrdccatin12lem2a  13728  swrdccatin2  13730  swrdccatin12lem2  13732  swrdccatin12  13734  swrdccat  13736  repswswrd  13774  repswccat  13775  cshwidxn  13798  cshweqdif2  13808  2cshwcshw  13814  cshwcshid  13816  cshwcsh2id  13817  f1oun2prg  13905  s2eq2s1eq  13924  s3eqs2s1eq  13926  wwlktovf1  13944  s3sndisj  13950  s3iunsndisj  13951  sqabsadd  14264  sqabssub  14265  abs2dif  14314  rexanuz  14327  o1of2  14585  o1rlimmul  14591  fsum2dlem  14743  isumltss  14821  fprodser  14919  fprodeq0  14945  fprod2dlem  14950  dvdscmulr  15252  dvdsmulcr  15253  summodnegmod  15254  dvds2ln  15256  dvdsflip  15281  divalglem9  15363  gcdcllem3  15461  gcdaddmlem  15483  gcdabs  15488  sqgcd  15516  lcmcllem  15547  lcmabs  15556  lcmgcdlem  15557  lcmgcd  15558  lcmgcdeq  15563  lcmf  15584  lcmftp  15587  lcmfunsnlem2lem1  15589  qredeq  15608  cncongr1  15618  cncongr2  15619  isprm7  15656  hashgcdlem  15729  pythagtriplem19  15774  dvdsprmpweqle  15826  difsqpwdvds  15827  prmgaplem4  15994  cshwsidrepsw  16031  setsfun0  16124  setsstruct2  16126  setsstructOLD  16129  xpsfrnel2  16449  isfunc  16747  fpwipodrs  17388  tsrss  17447  resmhm2  17584  gimco  17931  symg2bas  18038  pgrpsubgsymg  18048  symgextf  18057  gsmsymgrfixlem1  18067  fvcosymgeq  18069  gsmsymgreqlem1  18070  symgfixf1  18077  efgrelexlema  18382  gsum2dlem1  18589  gsum2dlem2  18590  dvdsr  18867  subrgpropd  19037  islmhm2  19264  ressmpladd  19685  ressmplmul  19686  mplind  19729  psgnghm  20152  psgndiflemB  20173  frlmbas3  20345  frlmphl  20350  islindf4  20407  mpt2matmul  20483  mavmul0g  20590  1marepvsma1  20620  mdetdiag  20636  slesolvec  20717  cramerimplem2  20723  cramerimplem3  20724  cramerimp  20725  mat2pmatlin  20773  m2pmfzgsumcl  20786  monmatcollpw  20817  pmatcollpw3lem  20821  pmatcollpwscmatlem1  20827  chpmat1dlem  20873  chfacfisf  20892  chfacfisfcpmat  20893  chfacfpmmulgsum2  20903  tgcl  21007  uncld  21079  innei  21163  cnco  21304  uncmp  21440  txbas  21604  txbasval  21643  tx1stc  21687  fbun  21877  infil  21900  fbunfip  21906  filuni  21922  imaelfm  21988  txflf  22043  tsmsfbas  22164  tsmsxp  22191  blin2  22467  nmhmplusg  22794  qtopbaslem  22795  iccntr  22857  ncvspi  23188  ncvs1  23189  unmbl  23540  volfiniun  23550  mbfi1flimlem  23725  ply1idom  24120  logreclem  24736  relogbcxpb  24761  fsumvma2  25175  chpchtsum  25180  dchrelbas3  25199  dchrmulcl  25210  lgsmulsqcoprm  25304  gausslemma2dlem1a  25326  lgsquad2lem2  25346  dchrisum0fmul  25431  dchrisum0lem1  25441  ishpg  25887  brcgr  26016  brbtwn2  26021  axcontlem2  26081  uspgredg2v  26353  usgredg2v  26356  usgr2v1e2w  26382  nb3gr2nb  26524  cusgredg  26570  cplgr3v  26581  cusgrop  26584  rusgr1vtx  26734  iswlkg  26759  wlkeq  26779  wlk1walk  26785  uspgr2wlkeq2  26793  uspgr2wlkeqi  26794  crctcshwlkn0lem3  26955  crctcshwlkn0lem4  26956  crctcshwlkn0lem5  26957  wspthneq1eq2  27009  wlkwwlkfunOLD  27045  wwlksnextinj  27058  2wlkdlem7  27094  2wlkdlem8  27095  2pthon3v  27105  s3wwlks2on  27119  elwwlks2  27130  elwspths2spth  27131  rusgrnumwwlks  27138  clwwlkccatlem  27154  clwlkclwwlklem2a  27163  clwlkclwwlklem3  27166  clwlkclwwlkf1lem2  27170  clwlkclwwlkf1  27175  clwlksf1clwwlkOLD  27265  clwwlknonex2  27300  3wlkdlem3  27356  uhgr3cyclex  27377  cusconngr  27386  eupth0  27409  frgr3v  27472  1to3vfriswmgr  27477  4cycl2v2nb  27486  frgrnbnb  27490  frgrncvvdeq  27506  frgrwopreglem4a  27507  frgrwopreglem5a  27508  frgrwopreglem4  27512  frgrwopreglem5  27518  frgrhash2wsp  27529  numclwwlk1lem2foa  27555  numclwwlk2  27583  numclwwlk2OLD  27590  blocni  28010  hvsub4  28244  shscli  28526  shscom  28528  spanunsni  28788  spanpr  28789  5oalem2  28864  5oalem3  28865  5oalem5  28867  3oalem1  28871  hoscl  28954  hoadddi  29012  hoadddir  29013  hosub4  29022  lnophsi  29210  hmops  29229  hmopm  29230  adjadd  29302  leop2  29333  leopadd  29341  leopmuli  29342  pjclem4  29408  pj3si  29416  mdslmd1lem2  29535  mdslmd3i  29541  atomli  29591  atcvatlem  29594  chirredlem3  29601  chirredi  29603  atcvat3i  29605  mdsymlem1  29612  mdsymlem5  29616  cdjreui  29641  cdj3i  29650  addltmulALT  29655  spc2ed  29662  mndpluscn  30319  sxbrsigalem5  30697  probfinmeasbOLD  30837  bnj545  31309  bnj546  31310  bnj557  31315  bnj570  31319  bnj594  31326  bnj1001  31372  bnj1118  31396  txpconn  31558  cvmlift2lem10  31638  lediv2aALT  31914  poseq  32095  frrlem5  32126  sltres  32157  nocvxminlem  32235  sslttr  32256  altopeq12  32411  altxpsspw  32426  funtransport  32480  neibastop1  32696  filnetlem3  32717  lukshef-ax2  32752  arg-ax  32753  nndivsub  32794  isbasisrelowllem1  33537  isbasisrelowllem2  33538  icoreclin  33539  relowlssretop  33545  rdgeqoa  33552  wl-ax11-lem2  33695  matunitlindflem1  33736  matunitlindflem2  33737  poimirlem4  33744  poimirlem26  33766  poimirlem29  33769  poimirlem30  33770  heicant  33775  mblfinlem1  33777  ismblfin  33781  itg2addnclem  33791  ftc1anclem6  33820  ftc1anclem7  33821  ftc1anclem8  33822  ftc1anc  33823  prdstotbnd  33922  heibor1lem  33937  isdrngo2  34086  divrngidl  34156  pridlc3  34201  linepsubN  35550  pmapsub  35566  elpaddri  35600  paddasslem14  35631  pmapjoin  35650  dvhfvadd  36889  dvhvaddcomN  36894  rmxynorm  38001  monotoddzzfi  38025  acongtr  38063  mpaaeu  38238  brfvrcld2  38501  rfovcnvf1od  38815  nzin  39034  pm10.14  39075  liminfvalxr  40512  etransclem38  40985  2reu4a  41718  2reu4  41719  tz6.12-afv2  41846  2elfz2melfz  41920  fz0addge0  41921  2ffzoeq  41930  icceuelpartlem  41963  icceuelpart  41964  pfxeq  41996  pfxsuffeqwrdeq  41998  pfxccat1  42002  pfxccatin12lem2  42016  pfxccatin12  42017  sqrtpwpw2p  42042  fmtnoprmfac1lem  42068  fmtnoprmfac1  42069  lighneallem2  42115  divgcdoddALTV  42185  gbowpos  42239  gbowgt5  42242  gboge9  42244  nnsum3primesgbe  42272  bgoldbtbndlem2  42286  bgoldbtbndlem3  42287  isupwlkg  42303  rabsubmgmd  42376  resmgmhm2  42384  ismhm0  42390  mhmismgmhm  42391  isrnghmmul  42478  c0ghm  42496  rhmisrnghm  42505  rnghmsubcsetclem2  42561  rngcinv  42566  rngcinvALTV  42578  rhmsubcsetclem2  42607  rhmsubcrngclem2  42613  ringcinv  42617  ringcinvALTV  42641  srhmsubc  42661  srhmsubcALTV  42679  mapprop  42709  zlmodzxzadd  42721  domnmsuppn0  42735  mndpfsupp  42742  ply1mulgsumlem2  42760  lincsum  42803  lincsumcl  42805  lincscmcl  42806  isldepslvec2  42859  modn0mul  42900  digexp  42986
  Copyright terms: Public domain W3C validator