Theorem anim12i 612

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

Step	Hyp	Ref	Expression
1		anim12i.1	. 2 ⊢ (𝜑 → 𝜓)
2		anim12i.2	. 2 ⊢ (𝜒 → 𝜃)
3		id 22	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 595	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 395

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 206  df-an 396

This theorem is referenced by:  anim12ci  613  anim1i  614  anim2i  616  anifp  1070  cgsex2g  3515  cgsex4g  3516  cgsex4gOLD  3517  cgsex4gOLDOLD  3518  spc2egv  3584  spc2ed  3586  sseq2  4004  uneqin  4274  2reu4lem  4521  2reu4  4522  disjpr2  4713  ssunieq  4941  iuneq1  5007  iuneq2  5010  copsex2t  5488  propeqop  5503  opthhausdorff  5513  opthhausdorff0  5514  iunopeqop  5517  soeq2  5606  opbrop  5769  xpsspw  5805  coeq1  5854  coeq2  5855  cnveq  5870  dmeq  5900  sotri  6127  tz7.7  6389  funun  6593  fununfun  6595  fundif  6596  funprg  6601  funtp  6604  2elresin  6670  funssxp  6746  fssres  6757  f1cof1  6798  f1coOLD  6800  foun  6851  f1un  6853  resdif  6854  f1oco  6856  fvun  6982  elfvmptrab1w  7026  elfvmptrab1  7027  fvn0ssdmfun  7078  dff3  7104  exfo  7109  fprg  7158  ftpg  7159  weisoeq2  7358  oprabv  7474  ndmovdistr  7604  ndmovord  7605  brrpssg  7724  eldifpw  7764  iunpw  7767  epweon  7771  bropfvvvv  8091  f1o2ndf1  8121  poseq  8157  fvn0elsupp  8178  wfrlem5OLD  8327  smores  8366  tz7.49  8459  tz7.49c  8460  oaord  8561  oeeulem  8615  nnaord  8633  brecop  8820  brecop2  8821  eroveu  8822  ecopovtrn  8830  ixpeq2  8921  undifixp  8944  undomOLD  9076  sbthlem8  9106  sbthlem9  9107  unxpdom  9269  isinf  9276  isinfOLD  9277  f1opwfi  9372  fiin  9437  en2lp  9621  inf3lem3  9645  brttrcl  9728  tcmin  9756  djuexb  9924  alephfp  10123  kmlem16  10180  endjudisj  10183  cofsmo  10284  fin23lem28  10355  axdc3lem2  10466  ac6c4  10496  brdom3  10543  brdom5  10544  brdom4  10545  canthp1lem2  10668  finngch  10670  ordpipq  10957  adderpq  10971  mulerpq  10972  lterpq  10985  genpn0  11018  genpnnp  11020  addclprlem2  11032  addcmpblnr  11084  addsrpr  11090  mulsrpr  11091  addclsr  11098  addasssr  11103  distrsr  11106  0idsr  11112  1idsr  11113  00sr  11114  mulgt0sr  11120  axaddf  11160  axaddass  11171  axdistr  11173  cnegex  11417  recextlem2  11867  difgtsumgt  12547  zaddcl  12624  qaddcl  12971  qmulcl  12973  qreccl  12975  xmulgt0  13286  xrsupsslem  13310  xrinfmsslem  13311  supxrpnf  13321  iccss  13416  difreicc  13485  fzadd2  13560  fzsubel  13561  ssfzunsnext  13570  difelfznle  13639  2ffzeq  13646  nelfzo  13661  fzonmapblen  13702  ubmelfzo  13721  ubmelm1fzo  13752  elfznelfzo  13761  subfzo0  13778  adddivflid  13807  modifeq2int  13922  modaddmodup  13923  addmodlteq  13935  fsuppmapnn0fiub  13980  mulexp  14090  mulexpz  14091  leexp1a  14163  faclbnd  14273  hashunx  14369  hashgt23el  14407  wrdeq  14510  ccatcl  14548  swrdnd  14628  swrdnd0  14631  swrdsbslen  14638  swrdspsleq  14639  pfxccat1  14676  swrdswrdlem  14678  pfxccatin12lem2a  14701  swrdccatin2  14703  pfxccatin12lem2  14705  pfxccatin12  14707  swrdccat  14709  reuccatpfxs1  14721  repswswrd  14758  repswccat  14760  cshwidxn  14783  cshweqdif2  14793  2cshwcshw  14800  cshwcshid  14802  cshwcsh2id  14803  f1oun2prg  14892  s2eq2s1eq  14911  s3eqs2s1eq  14913  s3sndisj  14938  s3iunsndisj  14939  sqabsadd  15253  sqabssub  15254  abs2dif  15303  rexanuz  15316  o1of2  15581  o1rlimmul  15587  fsum2dlem  15740  isumltss  15818  fprodser  15917  fprodeq0  15943  fprod2dlem  15948  dvdscmulr  16253  dvdsmulcr  16254  summodnegmod  16255  dvds2ln  16257  dvdsflip  16285  divalglem9  16369  gcdcllem3  16467  gcdaddmlem  16490  gcdabsOLD  16498  sqgcd  16527  lcmcllem  16558  lcmabs  16567  lcmgcdlem  16568  lcmgcd  16569  lcmgcdeq  16574  lcmftp  16598  lcmfunsnlem2lem1  16600  qredeq  16619  cncongr1  16629  cncongr2  16630  isprm7  16670  hashgcdlem  16748  dvdsprmpweqle  16846  difsqpwdvds  16847  prmgaplem4  17014  cshwsidrepsw  17054  setsfun0  17132  setsstruct2  17134  xpsfrnel2  17537  isfunc  17841  tsrss  18572  rabsubmgmd  18655  resmgmhm2  18663  ismhm0  18738  mhmismgmhm  18739  mndissubm  18750  resmndismnd  18751  resmhm2  18764  submefmnd  18838  sursubmefmnd  18839  injsubmefmnd  18840  grpissubg  19092  gimco  19213  symg2bas  19338  pgrpsubgsymg  19355  symgextf  19363  fvcosymgeq  19375  gsmsymgreqlem1  19376  symgfixf1  19383  efgrelexlema  19695  gsum2dlem1  19916  gsum2dlem2  19917  dvdsr  20290  isrnghmmul  20370  c0ghm  20389  rhmisrnghm  20408  subrngpropd  20494  subrgpropd  20536  rnghmsubcsetclem2  20554  rngcinv  20559  rhmsubcsetclem2  20583  rhmsubcrngclem2  20589  ringcinv  20593  srhmsubc  20602  islmhm2  20912  psgnghm  21499  psgndiflemB  21519  frlmbas3  21697  frlmphl  21702  islindf4  21759  ressmpladd  21954  ressmplmul  21955  mplind  22001  mpomatmul  22335  mavmul0g  22442  1marepvsma1  22472  mdetdiag  22488  slesolvec  22568  cramerimplem2  22573  cramerimplem3  22574  cramerimp  22575  mat2pmatlin  22624  m2pmfzgsumcl  22637  monmatcollpw  22668  pmatcollpw3lem  22672  pmatcollpwscmatlem1  22678  chpmat1dlem  22724  chfacfisf  22743  chfacfisfcpmat  22744  chfacfpmmulgsum2  22754  tgcl  22859  uncld  22932  innei  23016  cnco  23157  uncmp  23294  txbas  23458  txbasval  23497  tx1stc  23541  fbun  23731  infil  23754  fbunfip  23760  filuni  23776  imaelfm  23842  txflf  23897  tsmsfbas  24019  tsmsxp  24046  blin2  24322  nmhmplusg  24661  qtopbaslem  24662  iccntr  24724  ncvspi  25071  ncvs1  25072  unmbl  25453  volfiniun  25463  mbfi1flimlem  25639  ply1idom  26047  logreclem  26681  relogbcxpb  26706  fsumvma2  27134  chpchtsum  27139  dchrelbas3  27158  dchrmulcl  27169  lgsmulsqcoprm  27263  gausslemma2dlem1a  27285  lgsquad2lem2  27305  dchrisum0fmul  27426  dchrisum0lem1  27436  sltres  27582  nocvxminlem  27697  oldlim  27800  madebdayim  27801  madebdaylemlrcut  27812  readdscl  28214  remulscl  28217  ishpg  28550  brcgr  28698  brbtwn2  28703  axcontlem2  28763  uspgredg2v  29024  usgredg2v  29027  usgr2v1e2w  29052  nb3gr2nb  29184  cusgredg  29224  cplgr3v  29235  cusgrop  29238  rusgr1vtx  29389  iswlkg  29414  wlkeq  29435  wlk1walk  29440  uspgr2wlkeq2  29448  uspgr2wlkeqi  29449  crctcshwlkn0lem3  29610  crctcshwlkn0lem4  29611  crctcshwlkn0lem5  29612  wspthneq1eq2  29658  wwlksnextinj  29697  2wlkdlem7  29730  2wlkdlem8  29731  2pthon3v  29741  s3wwlks2on  29754  elwwlks2  29764  elwspths2spth  29765  rusgrnumwwlks  29772  clwlkclwwlklem2a  29795  clwlkclwwlklem3  29798  clwlkclwwlkf1lem2  29802  clwlkclwwlkf1  29807  clwwlknonex2  29906  3wlkdlem3  29958  uhgr3cyclex  29979  cusconngr  29988  eupth0  30011  frgr3v  30072  1to3vfriswmgr  30077  4cycl2v2nb  30086  frgrnbnb  30090  frgrncvvdeq  30106  frgrwopreglem4a  30107  frgrwopreglem5a  30108  frgrwopreglem4  30112  frgrwopreglem5  30118  frgrhash2wsp  30129  numclwwlk1lem2foa  30151  numclwwlk2  30178  blocni  30602  hvsub4  30834  shscli  31114  shscom  31116  spanunsni  31376  spanpr  31377  5oalem2  31452  5oalem3  31453  5oalem5  31455  3oalem1  31459  hoscl  31542  hoadddi  31600  hoadddir  31601  hosub4  31610  lnophsi  31798  hmops  31817  hmopm  31818  adjadd  31890  leop2  31921  leopadd  31929  leopmuli  31930  pjclem4  31996  pj3si  32004  mdslmd1lem2  32123  mdslmd3i  32129  atomli  32179  atcvatlem  32182  chirredlem3  32189  chirredi  32191  atcvat3i  32193  mdsymlem1  32200  mdsymlem5  32204  cdjreui  32229  cdj3i  32238  addltmulALT  32243  hashxpe  32560  mndpluscn  33463  sxbrsigalem5  33844  probfinmeasbALTV  33985  bnj545  34462  bnj546  34463  bnj557  34468  bnj570  34472  bnj594  34479  bnj1001  34526  bnj1118  34551  txpconn  34778  cvmlift2lem10  34858  gonar  34941  lediv2aALT  35217  altopeq12  35494  altxpsspw  35509  funtransport  35563  neibastop1  35779  filnetlem3  35800  lukshef-ax2  35835  arg-ax  35836  nndivsub  35877  bj-nnftht  36154  bj-nnfan  36161  bj-nnfor  36163  copsex2b  36555  isbasisrelowllem1  36770  isbasisrelowllem2  36771  icoreclin  36772  relowlssretop  36778  rdgeqoa  36785  fvineqsnf1  36825  wl-ax11-lem2  36988  matunitlindflem1  37024  matunitlindflem2  37025  poimirlem4  37032  poimirlem26  37054  poimirlem29  37057  poimirlem30  37058  heicant  37063  mblfinlem1  37065  ismblfin  37069  itg2addnclem  37079  ftc1anclem6  37106  ftc1anclem7  37107  ftc1anclem8  37108  ftc1anc  37109  prdstotbnd  37202  heibor1lem  37217  isdrngo2  37366  divrngidl  37436  pridlc3  37481  linepsubN  39162  pmapsub  39178  elpaddri  39212  paddasslem14  39243  pmapjoin  39262  dvhfvadd  40501  dvhvaddcomN  40506  imacrhmcl  41673  rimco  41677  rmxynorm  42261  monotoddzzfi  42285  acongtr  42321  mpaaeu  42496  oaltublim  42642  omord2lim  42652  cantnftermord  42672  dflim5  42681  omabs2  42684  tfsconcat0i  42697  ofoafo  42708  naddcnff  42714  oaun3lem1  42726  oaun3lem2  42727  pr2cv  42901  brfvrcld2  43045  rfovcnvf1od  43357  ismnushort  43661  nzin  43678  pm10.14  43719  disjrnmpt2  44484  liminfvalxr  45094  etransclem38  45583  cfsetsnfsetf1  46364  tz6.12-afv2  46543  2elfz2melfz  46621  fz0addge0  46622  2ffzoeq  46631  icceuelpartlem  46698  icceuelpart  46699  ich2exprop  46734  sqrtpwpw2p  46801  fmtnoprmfac1lem  46827  fmtnoprmfac1  46828  lighneallem2  46869  divgcdoddALTV  46945  gbowpos  47022  gbowgt5  47025  gboge9  47027  nnsum3primesgbe  47055  bgoldbtbndlem2  47069  bgoldbtbndlem3  47070  isupwlkg  47122  rngcinvALTV  47261  ringcinvALTV  47295  srhmsubcALTV  47310  mapprop  47333  zlmodzxzadd  47345  domnmsuppn0  47356  mndpfsupp  47363  ply1mulgsumlem2  47378  lincsum  47420  lincsumcl  47422  lincscmcl  47423  isldepslvec2  47476  modn0mul  47516  digexp  47603  rrx2pnecoorneor  47711  rrx2pnedifcoorneorr  47713  rrx2xpref1o  47714  ehl2eudis0lt  47722  rrx2linest  47738  line2x  47750  itsclc0yqsollem2  47759  seppsepf  47870  thincn0eu  47961