Theorem anim12i 613

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 596	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

Syntax hints:   → wi 4   ∧ wa 396

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 397

This theorem is referenced by:  anim12ci  614  anim1i  615  anim2i  617  anifp  1069  norassOLD  1536  cgsex2g  3476  cgsex4g  3477  cgsex4gOLD  3478  spc2egv  3539  spc2ed  3541  sseq2  3948  uneqin  4213  2reu4lem  4457  2reu4  4458  disjpr2  4650  ssunieq  4877  iuneq1  4941  iuneq2  4944  copsex2t  5407  propeqop  5422  opthhausdorff  5432  opthhausdorff0  5433  iunopeqop  5436  soeq2  5526  opbrop  5685  xpsspw  5721  coeq1  5769  coeq2  5770  cnveq  5785  dmeq  5815  sotri  6037  tz7.7  6296  funun  6487  fununfun  6489  fundif  6490  funprg  6495  funtp  6498  2elresin  6562  funssxp  6638  fssres  6649  f1cof1  6690  f1coOLD  6692  foun  6743  f1un  6745  resdif  6746  f1oco  6748  fvun  6867  elfvmptrab1w  6910  elfvmptrab1  6911  fvn0ssdmfun  6961  dff3  6985  exfo  6990  fprg  7036  ftpg  7037  weisoeq2  7236  oprabv  7344  ndmovdistr  7470  ndmovord  7471  brrpssg  7587  eldifpw  7627  iunpw  7630  epweon  7634  bropfvvvv  7941  f1o2ndf1  7972  fvn0elsupp  8005  wfrlem5OLD  8153  smores  8192  tz7.49  8285  tz7.49c  8286  oaord  8387  oeeulem  8441  nnaord  8459  brecop  8608  brecop2  8609  eroveu  8610  ecopovtrn  8618  ixpeq2  8708  undifixp  8731  undomOLD  8856  sbthlem8  8886  sbthlem9  8887  unxpdom  9039  isinf  9045  f1opwfi  9132  fiin  9190  en2lp  9373  inf3lem3  9397  brttrcl  9480  tcmin  9508  djuexb  9676  alephfp  9873  kmlem16  9930  endjudisj  9933  cofsmo  10034  fin23lem28  10105  axdc3lem2  10216  ac6c4  10246  brdom3  10293  brdom5  10294  brdom4  10295  canthp1lem2  10418  finngch  10420  ordpipq  10707  adderpq  10721  mulerpq  10722  lterpq  10735  genpn0  10768  genpnnp  10770  addclprlem2  10782  addcmpblnr  10834  addsrpr  10840  mulsrpr  10841  addclsr  10848  addasssr  10853  distrsr  10856  0idsr  10862  1idsr  10863  00sr  10864  mulgt0sr  10870  axaddf  10910  axaddass  10921  axdistr  10923  cnegex  11165  recextlem2  11615  difgtsumgt  12295  zaddcl  12369  qaddcl  12714  qmulcl  12716  qreccl  12718  xmulgt0  13026  xrsupsslem  13050  xrinfmsslem  13051  supxrpnf  13061  iccss  13156  difreicc  13225  fzadd2  13300  fzsubel  13301  ssfzunsnext  13310  difelfznle  13379  2ffzeq  13386  nelfzo  13401  fzonmapblen  13442  ubmelfzo  13461  ubmelm1fzo  13492  elfznelfzo  13501  subfzo0  13518  adddivflid  13547  modifeq2int  13662  modaddmodup  13663  addmodlteq  13675  fsuppmapnn0fiub  13720  mulexp  13831  mulexpz  13832  leexp1a  13902  faclbnd  14013  hashunx  14110  hashgt23el  14148  wrdeq  14248  ccatcl  14286  swrdnd  14376  swrdnd0  14379  swrdsbslen  14386  swrdspsleq  14387  pfxccat1  14424  swrdswrdlem  14426  pfxccatin12lem2a  14449  swrdccatin2  14451  pfxccatin12lem2  14453  pfxccatin12  14455  swrdccat  14457  reuccatpfxs1  14469  repswswrd  14506  repswccat  14508  cshwidxn  14531  cshweqdif2  14541  2cshwcshw  14547  cshwcshid  14549  cshwcsh2id  14550  f1oun2prg  14639  s2eq2s1eq  14658  s3eqs2s1eq  14660  s3sndisj  14687  s3iunsndisj  14688  sqabsadd  15003  sqabssub  15004  abs2dif  15053  rexanuz  15066  o1of2  15331  o1rlimmul  15337  fsum2dlem  15491  isumltss  15569  fprodser  15668  fprodeq0  15694  fprod2dlem  15699  dvdscmulr  16003  dvdsmulcr  16004  summodnegmod  16005  dvds2ln  16007  dvdsflip  16035  divalglem9  16119  gcdcllem3  16217  gcdaddmlem  16240  gcdabsOLD  16248  sqgcd  16279  lcmcllem  16310  lcmabs  16319  lcmgcdlem  16320  lcmgcd  16321  lcmgcdeq  16326  lcmftp  16350  lcmfunsnlem2lem1  16352  qredeq  16371  cncongr1  16381  cncongr2  16382  isprm7  16422  hashgcdlem  16498  dvdsprmpweqle  16596  difsqpwdvds  16597  prmgaplem4  16764  cshwsidrepsw  16804  setsfun0  16882  setsstruct2  16884  xpsfrnel2  17284  isfunc  17588  tsrss  18316  mndissubm  18455  resmndismnd  18456  resmhm2  18469  submefmnd  18543  sursubmefmnd  18544  injsubmefmnd  18545  grpissubg  18784  gimco  18893  symg2bas  19009  pgrpsubgsymg  19026  symgextf  19034  fvcosymgeq  19046  gsmsymgreqlem1  19047  symgfixf1  19054  efgrelexlema  19364  gsum2dlem1  19580  gsum2dlem2  19581  dvdsr  19897  subrgpropd  20068  islmhm2  20309  psgnghm  20794  psgndiflemB  20814  frlmbas3  20992  frlmphl  20997  islindf4  21054  ressmpladd  21239  ressmplmul  21240  mplind  21287  mpomatmul  21604  mavmul0g  21711  1marepvsma1  21741  mdetdiag  21757  slesolvec  21837  cramerimplem2  21842  cramerimplem3  21843  cramerimp  21844  mat2pmatlin  21893  m2pmfzgsumcl  21906  monmatcollpw  21937  pmatcollpw3lem  21941  pmatcollpwscmatlem1  21947  chpmat1dlem  21993  chfacfisf  22012  chfacfisfcpmat  22013  chfacfpmmulgsum2  22023  tgcl  22128  uncld  22201  innei  22285  cnco  22426  uncmp  22563  txbas  22727  txbasval  22766  tx1stc  22810  fbun  23000  infil  23023  fbunfip  23029  filuni  23045  imaelfm  23111  txflf  23166  tsmsfbas  23288  tsmsxp  23315  blin2  23591  nmhmplusg  23930  qtopbaslem  23931  iccntr  23993  ncvspi  24329  ncvs1  24330  unmbl  24710  volfiniun  24720  mbfi1flimlem  24896  ply1idom  25298  logreclem  25921  relogbcxpb  25946  fsumvma2  26371  chpchtsum  26376  dchrelbas3  26395  dchrmulcl  26406  lgsmulsqcoprm  26500  gausslemma2dlem1a  26522  lgsquad2lem2  26542  dchrisum0fmul  26663  dchrisum0lem1  26673  ishpg  27129  brcgr  27277  brbtwn2  27282  axcontlem2  27342  uspgredg2v  27600  usgredg2v  27603  usgr2v1e2w  27628  nb3gr2nb  27760  cusgredg  27800  cplgr3v  27811  cusgrop  27814  rusgr1vtx  27964  iswlkg  27989  wlkeq  28010  wlk1walk  28015  uspgr2wlkeq2  28023  uspgr2wlkeqi  28024  crctcshwlkn0lem3  28186  crctcshwlkn0lem4  28187  crctcshwlkn0lem5  28188  wspthneq1eq2  28234  wwlksnextinj  28273  2wlkdlem7  28306  2wlkdlem8  28307  2pthon3v  28317  s3wwlks2on  28330  elwwlks2  28340  elwspths2spth  28341  rusgrnumwwlks  28348  clwlkclwwlklem2a  28371  clwlkclwwlklem3  28374  clwlkclwwlkf1lem2  28378  clwlkclwwlkf1  28383  clwwlknonex2  28482  3wlkdlem3  28534  uhgr3cyclex  28555  cusconngr  28564  eupth0  28587  frgr3v  28648  1to3vfriswmgr  28653  4cycl2v2nb  28662  frgrnbnb  28666  frgrncvvdeq  28682  frgrwopreglem4a  28683  frgrwopreglem5a  28684  frgrwopreglem4  28688  frgrwopreglem5  28694  frgrhash2wsp  28705  numclwwlk1lem2foa  28727  numclwwlk2  28754  blocni  29176  hvsub4  29408  shscli  29688  shscom  29690  spanunsni  29950  spanpr  29951  5oalem2  30026  5oalem3  30027  5oalem5  30029  3oalem1  30033  hoscl  30116  hoadddi  30174  hoadddir  30175  hosub4  30184  lnophsi  30372  hmops  30391  hmopm  30392  adjadd  30464  leop2  30495  leopadd  30503  leopmuli  30504  pjclem4  30570  pj3si  30578  mdslmd1lem2  30697  mdslmd3i  30703  atomli  30753  atcvatlem  30756  chirredlem3  30763  chirredi  30765  atcvat3i  30767  mdsymlem1  30774  mdsymlem5  30778  cdjreui  30803  cdj3i  30812  addltmulALT  30817  hashxpe  31136  mndpluscn  31885  sxbrsigalem5  32264  probfinmeasbALTV  32405  bnj545  32884  bnj546  32885  bnj557  32890  bnj570  32894  bnj594  32901  bnj1001  32948  bnj1118  32973  txpconn  33203  cvmlift2lem10  33283  gonar  33366  lediv2aALT  33644  poseq  33811  sltres  33874  nocvxminlem  33981  oldlim  34078  madebdayim  34079  madebdaylemlrcut  34088  altopeq12  34273  altxpsspw  34288  funtransport  34342  neibastop1  34557  filnetlem3  34578  lukshef-ax2  34613  arg-ax  34614  nndivsub  34655  bj-nnftht  34932  bj-nnfan  34939  bj-nnfor  34941  copsex2b  35320  isbasisrelowllem1  35535  isbasisrelowllem2  35536  icoreclin  35537  relowlssretop  35543  rdgeqoa  35550  fvineqsnf1  35590  wl-ax11-lem2  35746  matunitlindflem1  35782  matunitlindflem2  35783  poimirlem4  35790  poimirlem26  35812  poimirlem29  35815  poimirlem30  35816  heicant  35821  mblfinlem1  35823  ismblfin  35827  itg2addnclem  35837  ftc1anclem6  35864  ftc1anclem7  35865  ftc1anclem8  35866  ftc1anc  35867  prdstotbnd  35961  heibor1lem  35976  isdrngo2  36125  divrngidl  36195  pridlc3  36240  linepsubN  37773  pmapsub  37789  elpaddri  37823  paddasslem14  37854  pmapjoin  37873  dvhfvadd  39112  dvhvaddcomN  39117  andiff  40166  rmxynorm  40747  monotoddzzfi  40771  acongtr  40807  mpaaeu  40982  pr2cv  41162  brfvrcld2  41307  rfovcnvf1od  41619  ismnushort  41926  nzin  41943  pm10.14  41984  disjrnmpt2  42733  liminfvalxr  43331  etransclem38  43820  cfsetsnfsetf1  44564  tz6.12-afv2  44743  2elfz2melfz  44821  fz0addge0  44822  2ffzoeq  44831  icceuelpartlem  44898  icceuelpart  44899  ich2exprop  44934  sqrtpwpw2p  45001  fmtnoprmfac1lem  45027  fmtnoprmfac1  45028  lighneallem2  45069  divgcdoddALTV  45145  gbowpos  45222  gbowgt5  45225  gboge9  45227  nnsum3primesgbe  45255  bgoldbtbndlem2  45269  bgoldbtbndlem3  45270  isupwlkg  45310  rabsubmgmd  45356  resmgmhm2  45364  ismhm0  45370  mhmismgmhm  45371  isrnghmmul  45462  c0ghm  45480  rhmisrnghm  45489  rnghmsubcsetclem2  45545  rngcinv  45550  rngcinvALTV  45562  rhmsubcsetclem2  45591  rhmsubcrngclem2  45597  ringcinv  45601  ringcinvALTV  45625  srhmsubc  45645  srhmsubcALTV  45663  mapprop  45693  zlmodzxzadd  45705  domnmsuppn0  45716  mndpfsupp  45723  ply1mulgsumlem2  45739  lincsum  45781  lincsumcl  45783  lincscmcl  45784  isldepslvec2  45837  modn0mul  45877  digexp  45964  rrx2pnecoorneor  46072  rrx2pnedifcoorneorr  46074  rrx2xpref1o  46075  ehl2eudis0lt  46083  rrx2linest  46099  line2x  46111  itsclc0yqsollem2  46120  seppsepf  46233  thincn0eu  46324