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

Theorem anim12i 615
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 598 1 ((𝜑𝜒) → (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399
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 210  df-an 400
This theorem is referenced by:  anim12ci  616  anim1i  617  anim2i  619  anifp  1067  norassOLD  1535  sbimiALT  2556  cgsex2g  3488  cgsex4g  3489  cgsex4gOLD  3490  spc2egv  3551  spc2ed  3553  sseq2  3944  uneqin  4208  2reu4lem  4426  2reu4  4427  disjpr2  4612  ssunieq  4838  iuneq1  4900  iuneq2  4903  copsex2t  5351  propeqop  5365  opthhausdorff  5375  opthhausdorff0  5376  iunopeqop  5379  soeq2  5463  opbrop  5616  xpsspw  5650  coeq1  5696  coeq2  5697  cnveq  5712  dmeq  5740  sotri  5958  tz7.7  6189  funun  6374  fununfun  6376  fundif  6377  funprg  6382  funtp  6385  2elresin  6444  funssxp  6513  fssres  6522  f1co  6564  foun  6612  resdif  6614  f1oco  6616  fvun  6732  elfvmptrab1w  6775  elfvmptrab1  6776  fvn0ssdmfun  6823  dff3  6847  exfo  6852  fprg  6898  ftpg  6899  weisoeq2  7092  oprabv  7197  ndmovdistr  7321  ndmovord  7322  brrpssg  7435  eldifpw  7474  iunpw  7477  bropfvvvv  7774  f1o2ndf1  7805  fvn0elsupp  7833  wfrlem5  7946  smores  7976  tz7.49  8068  tz7.49c  8069  oaord  8160  oeeulem  8214  nnaord  8232  brecop  8377  brecop2  8378  eroveu  8379  ecopovtrn  8387  ixpeq2  8462  undifixp  8485  undom  8592  sbthlem8  8622  sbthlem9  8623  unxpdom  8713  isinf  8719  f1opwfi  8816  fiin  8874  en2lp  9057  inf3lem3  9081  tcmin  9171  djuexb  9326  alephfp  9523  kmlem16  9580  endjudisj  9583  cofsmo  9684  fin23lem28  9755  axdc3lem2  9866  ac6c4  9896  brdom3  9943  brdom5  9944  brdom4  9945  canthp1lem2  10068  finngch  10070  ordpipq  10357  adderpq  10371  mulerpq  10372  lterpq  10385  genpn0  10418  genpnnp  10420  addclprlem2  10432  addcmpblnr  10484  addsrpr  10490  mulsrpr  10491  addclsr  10498  addasssr  10503  distrsr  10506  0idsr  10512  1idsr  10513  00sr  10514  mulgt0sr  10520  axaddf  10560  axaddass  10571  axdistr  10573  cnegex  10814  recextlem2  11264  difgtsumgt  11942  zaddcl  12014  qaddcl  12356  qmulcl  12358  qreccl  12360  xmulgt0  12668  xrsupsslem  12692  xrinfmsslem  12693  supxrpnf  12703  iccss  12797  difreicc  12866  fzadd2  12941  fzsubel  12942  ssfzunsnext  12951  difelfznle  13020  2ffzeq  13027  nelfzo  13042  fzonmapblen  13082  ubmelfzo  13101  ubmelm1fzo  13132  elfznelfzo  13141  subfzo0  13158  adddivflid  13187  modifeq2int  13300  modaddmodup  13301  addmodlteq  13313  fsuppmapnn0fiub  13358  mulexp  13468  mulexpz  13469  leexp1a  13539  faclbnd  13650  hashunx  13747  hashgt23el  13785  wrdeq  13883  ccatcl  13921  swrdnd  14011  swrdnd0  14014  swrdsbslen  14021  swrdspsleq  14022  pfxccat1  14059  swrdswrdlem  14061  pfxccatin12lem2a  14084  swrdccatin2  14086  pfxccatin12lem2  14088  pfxccatin12  14090  swrdccat  14092  reuccatpfxs1  14104  repswswrd  14141  repswccat  14143  cshwidxn  14166  cshweqdif2  14176  2cshwcshw  14182  cshwcshid  14184  cshwcsh2id  14185  f1oun2prg  14274  s2eq2s1eq  14293  s3eqs2s1eq  14295  s3sndisj  14322  s3iunsndisj  14323  sqabsadd  14637  sqabssub  14638  abs2dif  14687  rexanuz  14700  o1of2  14964  o1rlimmul  14970  fsum2dlem  15120  isumltss  15198  fprodser  15298  fprodeq0  15324  fprod2dlem  15329  dvdscmulr  15633  dvdsmulcr  15634  summodnegmod  15635  dvds2ln  15637  dvdsflip  15662  divalglem9  15745  gcdcllem3  15843  gcdaddmlem  15865  gcdabs  15870  sqgcd  15902  lcmcllem  15933  lcmabs  15942  lcmgcdlem  15943  lcmgcd  15944  lcmgcdeq  15949  lcmftp  15973  lcmfunsnlem2lem1  15975  qredeq  15994  cncongr1  16004  cncongr2  16005  isprm7  16045  hashgcdlem  16118  dvdsprmpweqle  16215  difsqpwdvds  16216  prmgaplem4  16383  cshwsidrepsw  16422  setsfun0  16514  setsstruct2  16516  xpsfrnel2  16832  isfunc  17129  tsrss  17828  mndissubm  17967  resmndismnd  17968  resmhm2  17981  submefmnd  18055  sursubmefmnd  18056  injsubmefmnd  18057  grpissubg  18294  gimco  18403  symg2bas  18516  pgrpsubgsymg  18532  symgextf  18540  fvcosymgeq  18552  gsmsymgreqlem1  18553  symgfixf1  18560  efgrelexlema  18870  gsum2dlem1  19086  gsum2dlem2  19087  dvdsr  19395  subrgpropd  19566  islmhm2  19806  psgnghm  20272  psgndiflemB  20292  frlmbas3  20468  frlmphl  20473  islindf4  20530  ressmpladd  20700  ressmplmul  20701  mplind  20744  mpomatmul  21054  mavmul0g  21161  1marepvsma1  21191  mdetdiag  21207  slesolvec  21287  cramerimplem2  21292  cramerimplem3  21293  cramerimp  21294  mat2pmatlin  21343  m2pmfzgsumcl  21356  monmatcollpw  21387  pmatcollpw3lem  21391  pmatcollpwscmatlem1  21397  chpmat1dlem  21443  chfacfisf  21462  chfacfisfcpmat  21463  chfacfpmmulgsum2  21473  tgcl  21577  uncld  21649  innei  21733  cnco  21874  uncmp  22011  txbas  22175  txbasval  22214  tx1stc  22258  fbun  22448  infil  22471  fbunfip  22477  filuni  22493  imaelfm  22559  txflf  22614  tsmsfbas  22736  tsmsxp  22763  blin2  23039  nmhmplusg  23366  qtopbaslem  23367  iccntr  23429  ncvspi  23764  ncvs1  23765  unmbl  24144  volfiniun  24154  mbfi1flimlem  24329  ply1idom  24728  logreclem  25351  relogbcxpb  25376  fsumvma2  25801  chpchtsum  25806  dchrelbas3  25825  dchrmulcl  25836  lgsmulsqcoprm  25930  gausslemma2dlem1a  25952  lgsquad2lem2  25972  dchrisum0fmul  26093  dchrisum0lem1  26103  ishpg  26556  brcgr  26697  brbtwn2  26702  axcontlem2  26762  uspgredg2v  27017  usgredg2v  27020  usgr2v1e2w  27045  nb3gr2nb  27177  cusgredg  27217  cplgr3v  27228  cusgrop  27231  rusgr1vtx  27381  iswlkg  27406  wlkeq  27426  wlk1walk  27431  uspgr2wlkeq2  27439  uspgr2wlkeqi  27440  crctcshwlkn0lem3  27601  crctcshwlkn0lem4  27602  crctcshwlkn0lem5  27603  wspthneq1eq2  27649  wwlksnextinj  27688  2wlkdlem7  27721  2wlkdlem8  27722  2pthon3v  27732  s3wwlks2on  27745  elwwlks2  27755  elwspths2spth  27756  rusgrnumwwlks  27763  clwlkclwwlklem2a  27786  clwlkclwwlklem3  27789  clwlkclwwlkf1lem2  27793  clwlkclwwlkf1  27798  clwwlknonex2  27897  3wlkdlem3  27949  uhgr3cyclex  27970  cusconngr  27979  eupth0  28002  frgr3v  28063  1to3vfriswmgr  28068  4cycl2v2nb  28077  frgrnbnb  28081  frgrncvvdeq  28097  frgrwopreglem4a  28098  frgrwopreglem5a  28099  frgrwopreglem4  28103  frgrwopreglem5  28109  frgrhash2wsp  28120  numclwwlk1lem2foa  28142  numclwwlk2  28169  blocni  28591  hvsub4  28823  shscli  29103  shscom  29105  spanunsni  29365  spanpr  29366  5oalem2  29441  5oalem3  29442  5oalem5  29444  3oalem1  29448  hoscl  29531  hoadddi  29589  hoadddir  29590  hosub4  29599  lnophsi  29787  hmops  29806  hmopm  29807  adjadd  29879  leop2  29910  leopadd  29918  leopmuli  29919  pjclem4  29985  pj3si  29993  mdslmd1lem2  30112  mdslmd3i  30118  atomli  30168  atcvatlem  30171  chirredlem3  30178  chirredi  30180  atcvat3i  30182  mdsymlem1  30189  mdsymlem5  30193  cdjreui  30218  cdj3i  30227  addltmulALT  30232  hashxpe  30558  mndpluscn  31277  sxbrsigalem5  31654  probfinmeasbALTV  31795  bnj545  32275  bnj546  32276  bnj557  32281  bnj570  32285  bnj594  32292  bnj1001  32339  bnj1118  32364  txpconn  32587  cvmlift2lem10  32667  gonar  32750  lediv2aALT  33028  poseq  33203  sltres  33277  nocvxminlem  33355  sslttr  33376  altopeq12  33531  altxpsspw  33546  funtransport  33600  neibastop1  33815  filnetlem3  33836  lukshef-ax2  33871  arg-ax  33872  nndivsub  33913  bj-nnftht  34180  bj-nnfan  34187  bj-nnfor  34189  copsex2b  34550  isbasisrelowllem1  34767  isbasisrelowllem2  34768  icoreclin  34769  relowlssretop  34775  rdgeqoa  34782  fvineqsnf1  34822  wl-ax11-lem2  34976  matunitlindflem1  35046  matunitlindflem2  35047  poimirlem4  35054  poimirlem26  35076  poimirlem29  35079  poimirlem30  35080  heicant  35085  mblfinlem1  35087  ismblfin  35091  itg2addnclem  35101  ftc1anclem6  35128  ftc1anclem7  35129  ftc1anclem8  35130  ftc1anc  35131  prdstotbnd  35225  heibor1lem  35240  isdrngo2  35389  divrngidl  35459  pridlc3  35504  linepsubN  37041  pmapsub  37057  elpaddri  37091  paddasslem14  37122  pmapjoin  37141  dvhfvadd  38380  dvhvaddcomN  38385  andiff  39371  rmxynorm  39846  monotoddzzfi  39870  acongtr  39906  mpaaeu  40081  pr2cv  40234  brfvrcld2  40380  rfovcnvf1od  40692  nzin  41009  pm10.14  41050  disjrnmpt2  41802  liminfvalxr  42412  etransclem38  42901  tz6.12-afv2  43783  2elfz2melfz  43862  fz0addge0  43863  2ffzoeq  43872  icceuelpartlem  43939  icceuelpart  43940  ich2exprop  43975  sqrtpwpw2p  44042  fmtnoprmfac1lem  44068  fmtnoprmfac1  44069  lighneallem2  44111  divgcdoddALTV  44187  gbowpos  44264  gbowgt5  44267  gboge9  44269  nnsum3primesgbe  44297  bgoldbtbndlem2  44311  bgoldbtbndlem3  44312  isupwlkg  44352  rabsubmgmd  44398  resmgmhm2  44406  ismhm0  44412  mhmismgmhm  44413  isrnghmmul  44504  c0ghm  44522  rhmisrnghm  44531  rnghmsubcsetclem2  44587  rngcinv  44592  rngcinvALTV  44604  rhmsubcsetclem2  44633  rhmsubcrngclem2  44639  ringcinv  44643  ringcinvALTV  44667  srhmsubc  44687  srhmsubcALTV  44705  mapprop  44735  zlmodzxzadd  44747  domnmsuppn0  44758  mndpfsupp  44765  ply1mulgsumlem2  44782  lincsum  44825  lincsumcl  44827  lincscmcl  44828  isldepslvec2  44881  modn0mul  44921  digexp  45008  rrx2pnecoorneor  45116  rrx2pnedifcoorneorr  45118  rrx2xpref1o  45119  ehl2eudis0lt  45127  rrx2linest  45143  line2x  45155  itsclc0yqsollem2  45164
  Copyright terms: Public domain W3C validator