Theorem anim12i 614

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  anim12ci  615  anim1i  616  anim2i  618  anifp  1065  norassOLD  1534  sbimiOLD  2515  sbimiALT  2577  cgsex2g  3538  cgsex4g  3539  spc2egv  3600  spc2ed  3602  sseq2  3993  uneqin  4255  2reu4lem  4465  2reu4  4466  disjpr2  4649  ssunieq  4873  iuneq1  4935  iuneq2  4938  copsex2t  5383  propeqop  5397  opthhausdorff  5407  opthhausdorff0  5408  iunopeqop  5411  soeq2  5495  opbrop  5648  xpsspw  5682  coeq1  5728  coeq2  5729  cnveq  5744  dmeq  5772  sotri  5987  tz7.7  6217  funun  6400  fununfun  6402  fundif  6403  funprg  6408  funtp  6411  2elresin  6468  funssxp  6535  fssres  6544  f1co  6585  foun  6633  resdif  6635  f1oco  6637  fvun  6753  elfvmptrab1w  6794  elfvmptrab1  6795  fvn0ssdmfun  6842  dff3  6866  exfo  6871  fprg  6917  ftpg  6918  weisoeq2  7109  oprabv  7214  ndmovdistr  7337  ndmovord  7338  brrpssg  7451  eldifpw  7490  iunpw  7493  bropfvvvv  7787  f1o2ndf1  7818  fvn0elsupp  7846  wfrlem5  7959  smores  7989  tz7.49  8081  tz7.49c  8082  oaord  8173  oeeulem  8227  nnaord  8245  brecop  8390  brecop2  8391  eroveu  8392  ecopovtrn  8400  ixpeq2  8475  undifixp  8498  undom  8605  sbthlem8  8634  sbthlem9  8635  unxpdom  8725  isinf  8731  f1opwfi  8828  fiin  8886  en2lp  9069  inf3lem3  9093  tcmin  9183  djuexb  9338  alephfp  9534  kmlem16  9591  endjudisj  9594  cofsmo  9691  fin23lem28  9762  axdc3lem2  9873  ac6c4  9903  brdom3  9950  brdom5  9951  brdom4  9952  canthp1lem2  10075  finngch  10077  ordpipq  10364  adderpq  10378  mulerpq  10379  lterpq  10392  genpn0  10425  genpnnp  10427  addclprlem2  10439  addcmpblnr  10491  addsrpr  10497  mulsrpr  10498  addclsr  10505  addasssr  10510  distrsr  10513  0idsr  10519  1idsr  10520  00sr  10521  mulgt0sr  10527  axaddf  10567  axaddass  10578  axdistr  10580  cnegex  10821  recextlem2  11271  difgtsumgt  11951  zaddcl  12023  qaddcl  12365  qmulcl  12367  qreccl  12369  xmulgt0  12677  xrsupsslem  12701  xrinfmsslem  12702  supxrpnf  12712  iccss  12805  difreicc  12871  fzadd2  12943  fzsubel  12944  ssfzunsnext  12953  difelfznle  13022  2ffzeq  13029  nelfzo  13044  fzonmapblen  13084  ubmelfzo  13103  ubmelm1fzo  13134  elfznelfzo  13143  subfzo0  13160  adddivflid  13189  modifeq2int  13302  modaddmodup  13303  addmodlteq  13315  fsuppmapnn0fiub  13360  mulexp  13469  mulexpz  13470  leexp1a  13540  faclbnd  13651  hashunx  13748  hashgt23el  13786  wrdeq  13886  ccatcl  13926  swrdnd  14016  swrdnd0  14019  swrdsbslen  14026  swrdspsleq  14027  pfxccat1  14064  swrdswrdlem  14066  pfxccatin12lem2a  14089  swrdccatin2  14091  pfxccatin12lem2  14093  pfxccatin12  14095  swrdccat  14097  reuccatpfxs1  14109  repswswrd  14146  repswccat  14148  cshwidxn  14171  cshweqdif2  14181  2cshwcshw  14187  cshwcshid  14189  cshwcsh2id  14190  f1oun2prg  14279  s2eq2s1eq  14298  s3eqs2s1eq  14300  s3sndisj  14327  s3iunsndisj  14328  sqabsadd  14642  sqabssub  14643  abs2dif  14692  rexanuz  14705  o1of2  14969  o1rlimmul  14975  fsum2dlem  15125  isumltss  15203  fprodser  15303  fprodeq0  15329  fprod2dlem  15334  dvdscmulr  15638  dvdsmulcr  15639  summodnegmod  15640  dvds2ln  15642  dvdsflip  15667  divalglem9  15752  gcdcllem3  15850  gcdaddmlem  15872  gcdabs  15877  sqgcd  15909  lcmcllem  15940  lcmabs  15949  lcmgcdlem  15950  lcmgcd  15951  lcmgcdeq  15956  lcmftp  15980  lcmfunsnlem2lem1  15982  qredeq  16001  cncongr1  16011  cncongr2  16012  isprm7  16052  hashgcdlem  16125  dvdsprmpweqle  16222  difsqpwdvds  16223  prmgaplem4  16390  cshwsidrepsw  16427  setsfun0  16519  setsstruct2  16521  xpsfrnel2  16837  isfunc  17134  tsrss  17833  mndissubm  17972  resmndismnd  17973  resmhm2  17986  submefmnd  18060  sursubmefmnd  18061  injsubmefmnd  18062  grpissubg  18299  gimco  18408  symg2bas  18521  pgrpsubgsymg  18537  symgextf  18545  fvcosymgeq  18557  gsmsymgreqlem1  18558  symgfixf1  18565  efgrelexlema  18875  gsum2dlem1  19090  gsum2dlem2  19091  dvdsr  19396  subrgpropd  19570  islmhm2  19810  ressmpladd  20238  ressmplmul  20239  mplind  20282  psgnghm  20724  psgndiflemB  20744  frlmbas3  20920  frlmphl  20925  islindf4  20982  mpomatmul  21055  mavmul0g  21162  1marepvsma1  21192  mdetdiag  21208  slesolvec  21288  cramerimplem2  21293  cramerimplem3  21294  cramerimp  21295  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  23760  ncvs1  23761  unmbl  24138  volfiniun  24148  mbfi1flimlem  24323  ply1idom  24718  logreclem  25340  relogbcxpb  25365  fsumvma2  25790  chpchtsum  25795  dchrelbas3  25814  dchrmulcl  25825  lgsmulsqcoprm  25919  gausslemma2dlem1a  25941  lgsquad2lem2  25961  dchrisum0fmul  26082  dchrisum0lem1  26092  ishpg  26545  brcgr  26686  brbtwn2  26691  axcontlem2  26751  uspgredg2v  27006  usgredg2v  27009  usgr2v1e2w  27034  nb3gr2nb  27166  cusgredg  27206  cplgr3v  27217  cusgrop  27220  rusgr1vtx  27370  iswlkg  27395  wlkeq  27415  wlk1walk  27420  uspgr2wlkeq2  27428  uspgr2wlkeqi  27429  crctcshwlkn0lem3  27590  crctcshwlkn0lem4  27591  crctcshwlkn0lem5  27592  wspthneq1eq2  27638  wwlksnextinj  27677  2wlkdlem7  27711  2wlkdlem8  27712  2pthon3v  27722  s3wwlks2on  27735  elwwlks2  27745  elwspths2spth  27746  rusgrnumwwlks  27753  clwlkclwwlklem2a  27776  clwlkclwwlklem3  27779  clwlkclwwlkf1lem2  27783  clwlkclwwlkf1  27788  clwwlknonex2  27888  3wlkdlem3  27940  uhgr3cyclex  27961  cusconngr  27970  eupth0  27993  frgr3v  28054  1to3vfriswmgr  28059  4cycl2v2nb  28068  frgrnbnb  28072  frgrncvvdeq  28088  frgrwopreglem4a  28089  frgrwopreglem5a  28090  frgrwopreglem4  28094  frgrwopreglem5  28100  frgrhash2wsp  28111  numclwwlk1lem2foa  28133  numclwwlk2  28160  blocni  28582  hvsub4  28814  shscli  29094  shscom  29096  spanunsni  29356  spanpr  29357  5oalem2  29432  5oalem3  29433  5oalem5  29435  3oalem1  29439  hoscl  29522  hoadddi  29580  hoadddir  29581  hosub4  29590  lnophsi  29778  hmops  29797  hmopm  29798  adjadd  29870  leop2  29901  leopadd  29909  leopmuli  29910  pjclem4  29976  pj3si  29984  mdslmd1lem2  30103  mdslmd3i  30109  atomli  30159  atcvatlem  30162  chirredlem3  30169  chirredi  30171  atcvat3i  30173  mdsymlem1  30180  mdsymlem5  30184  cdjreui  30209  cdj3i  30218  addltmulALT  30223  hashxpe  30529  mndpluscn  31169  sxbrsigalem5  31546  probfinmeasbALTV  31687  bnj545  32167  bnj546  32168  bnj557  32173  bnj570  32177  bnj594  32184  bnj1001  32231  bnj1118  32256  txpconn  32479  cvmlift2lem10  32559  gonar  32642  lediv2aALT  32920  poseq  33095  sltres  33169  nocvxminlem  33247  sslttr  33268  altopeq12  33423  altxpsspw  33438  funtransport  33492  neibastop1  33707  filnetlem3  33728  lukshef-ax2  33763  arg-ax  33764  nndivsub  33805  bj-nnftht  34070  bj-nnfan  34077  bj-nnfor  34079  copsex2b  34435  isbasisrelowllem1  34639  isbasisrelowllem2  34640  icoreclin  34641  relowlssretop  34647  rdgeqoa  34654  fvineqsnf1  34694  wl-ax11-lem2  34833  matunitlindflem1  34903  matunitlindflem2  34904  poimirlem4  34911  poimirlem26  34933  poimirlem29  34936  poimirlem30  34937  heicant  34942  mblfinlem1  34944  ismblfin  34948  itg2addnclem  34958  ftc1anclem6  34987  ftc1anclem7  34988  ftc1anclem8  34989  ftc1anc  34990  prdstotbnd  35087  heibor1lem  35102  isdrngo2  35251  divrngidl  35321  pridlc3  35366  linepsubN  36903  pmapsub  36919  elpaddri  36953  paddasslem14  36984  pmapjoin  37003  dvhfvadd  38242  dvhvaddcomN  38247  andiff  39142  rmxynorm  39564  monotoddzzfi  39588  acongtr  39624  mpaaeu  39799  pr2cv  39956  brfvrcld2  40086  rfovcnvf1od  40399  nzin  40699  pm10.14  40740  disjrnmpt2  41498  liminfvalxr  42113  etransclem38  42606  tz6.12-afv2  43488  2elfz2melfz  43567  fz0addge0  43568  2ffzoeq  43577  icceuelpartlem  43644  icceuelpart  43645  ich2exprop  43682  sqrtpwpw2p  43749  fmtnoprmfac1lem  43775  fmtnoprmfac1  43776  lighneallem2  43820  divgcdoddALTV  43896  gbowpos  43973  gbowgt5  43976  gboge9  43978  nnsum3primesgbe  44006  bgoldbtbndlem2  44020  bgoldbtbndlem3  44021  isupwlkg  44061  rabsubmgmd  44107  resmgmhm2  44115  ismhm0  44121  mhmismgmhm  44122  isrnghmmul  44213  c0ghm  44231  rhmisrnghm  44240  rnghmsubcsetclem2  44296  rngcinv  44301  rngcinvALTV  44313  rhmsubcsetclem2  44342  rhmsubcrngclem2  44348  ringcinv  44352  ringcinvALTV  44376  srhmsubc  44396  srhmsubcALTV  44414  mapprop  44443  zlmodzxzadd  44455  domnmsuppn0  44466  mndpfsupp  44473  ply1mulgsumlem2  44490  lincsum  44533  lincsumcl  44535  lincscmcl  44536  isldepslvec2  44589  modn0mul  44629  digexp  44716  rrx2pnecoorneor  44751  rrx2pnedifcoorneorr  44753  rrx2xpref1o  44754  ehl2eudis0lt  44762  rrx2linest  44778  line2x  44790  itsclc0yqsollem2  44799