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 397

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 398

This theorem is referenced by:  anim12ci  615  anim1i  616  anim2i  618  anifp  1071  cgsex2g  3520  cgsex4g  3521  cgsex4gOLD  3522  cgsex4gOLDOLD  3523  spc2egv  3590  spc2ed  3592  sseq2  4009  uneqin  4279  2reu4lem  4526  2reu4  4527  disjpr2  4718  ssunieq  4948  iuneq1  5014  iuneq2  5017  copsex2t  5493  propeqop  5508  opthhausdorff  5518  opthhausdorff0  5519  iunopeqop  5522  soeq2  5611  opbrop  5774  xpsspw  5810  coeq1  5858  coeq2  5859  cnveq  5874  dmeq  5904  sotri  6129  tz7.7  6391  funun  6595  fununfun  6597  fundif  6598  funprg  6603  funtp  6606  2elresin  6672  funssxp  6747  fssres  6758  f1cof1  6799  f1coOLD  6801  foun  6852  f1un  6854  resdif  6855  f1oco  6857  fvun  6982  elfvmptrab1w  7025  elfvmptrab1  7026  fvn0ssdmfun  7077  dff3  7102  exfo  7107  fprg  7153  ftpg  7154  weisoeq2  7353  oprabv  7469  ndmovdistr  7596  ndmovord  7597  brrpssg  7715  eldifpw  7755  iunpw  7758  epweon  7762  bropfvvvv  8078  f1o2ndf1  8108  poseq  8144  fvn0elsupp  8165  wfrlem5OLD  8313  smores  8352  tz7.49  8445  tz7.49c  8446  oaord  8547  oeeulem  8601  nnaord  8619  brecop  8804  brecop2  8805  eroveu  8806  ecopovtrn  8814  ixpeq2  8905  undifixp  8928  undomOLD  9060  sbthlem8  9090  sbthlem9  9091  unxpdom  9253  isinf  9260  isinfOLD  9261  f1opwfi  9356  fiin  9417  en2lp  9601  inf3lem3  9625  brttrcl  9708  tcmin  9736  djuexb  9904  alephfp  10103  kmlem16  10160  endjudisj  10163  cofsmo  10264  fin23lem28  10335  axdc3lem2  10446  ac6c4  10476  brdom3  10523  brdom5  10524  brdom4  10525  canthp1lem2  10648  finngch  10650  ordpipq  10937  adderpq  10951  mulerpq  10952  lterpq  10965  genpn0  10998  genpnnp  11000  addclprlem2  11012  addcmpblnr  11064  addsrpr  11070  mulsrpr  11071  addclsr  11078  addasssr  11083  distrsr  11086  0idsr  11092  1idsr  11093  00sr  11094  mulgt0sr  11100  axaddf  11140  axaddass  11151  axdistr  11153  cnegex  11395  recextlem2  11845  difgtsumgt  12525  zaddcl  12602  qaddcl  12949  qmulcl  12951  qreccl  12953  xmulgt0  13262  xrsupsslem  13286  xrinfmsslem  13287  supxrpnf  13297  iccss  13392  difreicc  13461  fzadd2  13536  fzsubel  13537  ssfzunsnext  13546  difelfznle  13615  2ffzeq  13622  nelfzo  13637  fzonmapblen  13678  ubmelfzo  13697  ubmelm1fzo  13728  elfznelfzo  13737  subfzo0  13754  adddivflid  13783  modifeq2int  13898  modaddmodup  13899  addmodlteq  13911  fsuppmapnn0fiub  13956  mulexp  14067  mulexpz  14068  leexp1a  14140  faclbnd  14250  hashunx  14346  hashgt23el  14384  wrdeq  14486  ccatcl  14524  swrdnd  14604  swrdnd0  14607  swrdsbslen  14614  swrdspsleq  14615  pfxccat1  14652  swrdswrdlem  14654  pfxccatin12lem2a  14677  swrdccatin2  14679  pfxccatin12lem2  14681  pfxccatin12  14683  swrdccat  14685  reuccatpfxs1  14697  repswswrd  14734  repswccat  14736  cshwidxn  14759  cshweqdif2  14769  2cshwcshw  14776  cshwcshid  14778  cshwcsh2id  14779  f1oun2prg  14868  s2eq2s1eq  14887  s3eqs2s1eq  14889  s3sndisj  14914  s3iunsndisj  14915  sqabsadd  15229  sqabssub  15230  abs2dif  15279  rexanuz  15292  o1of2  15557  o1rlimmul  15563  fsum2dlem  15716  isumltss  15794  fprodser  15893  fprodeq0  15919  fprod2dlem  15924  dvdscmulr  16228  dvdsmulcr  16229  summodnegmod  16230  dvds2ln  16232  dvdsflip  16260  divalglem9  16344  gcdcllem3  16442  gcdaddmlem  16465  gcdabsOLD  16473  sqgcd  16502  lcmcllem  16533  lcmabs  16542  lcmgcdlem  16543  lcmgcd  16544  lcmgcdeq  16549  lcmftp  16573  lcmfunsnlem2lem1  16575  qredeq  16594  cncongr1  16604  cncongr2  16605  isprm7  16645  hashgcdlem  16721  dvdsprmpweqle  16819  difsqpwdvds  16820  prmgaplem4  16987  cshwsidrepsw  17027  setsfun0  17105  setsstruct2  17107  xpsfrnel2  17510  isfunc  17814  tsrss  18542  mndissubm  18688  resmndismnd  18689  resmhm2  18702  submefmnd  18776  sursubmefmnd  18777  injsubmefmnd  18778  grpissubg  19026  gimco  19142  symg2bas  19260  pgrpsubgsymg  19277  symgextf  19285  fvcosymgeq  19297  gsmsymgreqlem1  19298  symgfixf1  19305  efgrelexlema  19617  gsum2dlem1  19838  gsum2dlem2  19839  dvdsr  20176  subrgpropd  20355  islmhm2  20649  psgnghm  21133  psgndiflemB  21153  frlmbas3  21331  frlmphl  21336  islindf4  21393  ressmpladd  21584  ressmplmul  21585  mplind  21631  mpomatmul  21948  mavmul0g  22055  1marepvsma1  22085  mdetdiag  22101  slesolvec  22181  cramerimplem2  22186  cramerimplem3  22187  cramerimp  22188  mat2pmatlin  22237  m2pmfzgsumcl  22250  monmatcollpw  22281  pmatcollpw3lem  22285  pmatcollpwscmatlem1  22291  chpmat1dlem  22337  chfacfisf  22356  chfacfisfcpmat  22357  chfacfpmmulgsum2  22367  tgcl  22472  uncld  22545  innei  22629  cnco  22770  uncmp  22907  txbas  23071  txbasval  23110  tx1stc  23154  fbun  23344  infil  23367  fbunfip  23373  filuni  23389  imaelfm  23455  txflf  23510  tsmsfbas  23632  tsmsxp  23659  blin2  23935  nmhmplusg  24274  qtopbaslem  24275  iccntr  24337  ncvspi  24673  ncvs1  24674  unmbl  25054  volfiniun  25064  mbfi1flimlem  25240  ply1idom  25642  logreclem  26267  relogbcxpb  26292  fsumvma2  26717  chpchtsum  26722  dchrelbas3  26741  dchrmulcl  26752  lgsmulsqcoprm  26846  gausslemma2dlem1a  26868  lgsquad2lem2  26888  dchrisum0fmul  27009  dchrisum0lem1  27019  sltres  27165  nocvxminlem  27279  oldlim  27381  madebdayim  27382  madebdaylemlrcut  27393  ishpg  28010  brcgr  28158  brbtwn2  28163  axcontlem2  28223  uspgredg2v  28481  usgredg2v  28484  usgr2v1e2w  28509  nb3gr2nb  28641  cusgredg  28681  cplgr3v  28692  cusgrop  28695  rusgr1vtx  28845  iswlkg  28870  wlkeq  28891  wlk1walk  28896  uspgr2wlkeq2  28904  uspgr2wlkeqi  28905  crctcshwlkn0lem3  29066  crctcshwlkn0lem4  29067  crctcshwlkn0lem5  29068  wspthneq1eq2  29114  wwlksnextinj  29153  2wlkdlem7  29186  2wlkdlem8  29187  2pthon3v  29197  s3wwlks2on  29210  elwwlks2  29220  elwspths2spth  29221  rusgrnumwwlks  29228  clwlkclwwlklem2a  29251  clwlkclwwlklem3  29254  clwlkclwwlkf1lem2  29258  clwlkclwwlkf1  29263  clwwlknonex2  29362  3wlkdlem3  29414  uhgr3cyclex  29435  cusconngr  29444  eupth0  29467  frgr3v  29528  1to3vfriswmgr  29533  4cycl2v2nb  29542  frgrnbnb  29546  frgrncvvdeq  29562  frgrwopreglem4a  29563  frgrwopreglem5a  29564  frgrwopreglem4  29568  frgrwopreglem5  29574  frgrhash2wsp  29585  numclwwlk1lem2foa  29607  numclwwlk2  29634  blocni  30058  hvsub4  30290  shscli  30570  shscom  30572  spanunsni  30832  spanpr  30833  5oalem2  30908  5oalem3  30909  5oalem5  30911  3oalem1  30915  hoscl  30998  hoadddi  31056  hoadddir  31057  hosub4  31066  lnophsi  31254  hmops  31273  hmopm  31274  adjadd  31346  leop2  31377  leopadd  31385  leopmuli  31386  pjclem4  31452  pj3si  31460  mdslmd1lem2  31579  mdslmd3i  31585  atomli  31635  atcvatlem  31638  chirredlem3  31645  chirredi  31647  atcvat3i  31649  mdsymlem1  31656  mdsymlem5  31660  cdjreui  31685  cdj3i  31694  addltmulALT  31699  hashxpe  32019  mndpluscn  32906  sxbrsigalem5  33287  probfinmeasbALTV  33428  bnj545  33906  bnj546  33907  bnj557  33912  bnj570  33916  bnj594  33923  bnj1001  33970  bnj1118  33995  txpconn  34223  cvmlift2lem10  34303  gonar  34386  lediv2aALT  34662  altopeq12  34934  altxpsspw  34949  funtransport  35003  neibastop1  35244  filnetlem3  35265  lukshef-ax2  35300  arg-ax  35301  nndivsub  35342  bj-nnftht  35619  bj-nnfan  35626  bj-nnfor  35628  copsex2b  36021  isbasisrelowllem1  36236  isbasisrelowllem2  36237  icoreclin  36238  relowlssretop  36244  rdgeqoa  36251  fvineqsnf1  36291  wl-ax11-lem2  36448  matunitlindflem1  36484  matunitlindflem2  36485  poimirlem4  36492  poimirlem26  36514  poimirlem29  36517  poimirlem30  36518  heicant  36523  mblfinlem1  36525  ismblfin  36529  itg2addnclem  36539  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anclem8  36568  ftc1anc  36569  prdstotbnd  36662  heibor1lem  36677  isdrngo2  36826  divrngidl  36896  pridlc3  36941  linepsubN  38623  pmapsub  38639  elpaddri  38673  paddasslem14  38704  pmapjoin  38723  dvhfvadd  39962  dvhvaddcomN  39967  andiff  41019  imacrhmcl  41089  rimco  41093  rmxynorm  41657  monotoddzzfi  41681  acongtr  41717  mpaaeu  41892  oaltublim  42040  omord2lim  42050  cantnftermord  42070  dflim5  42079  omabs2  42082  tfsconcat0i  42095  ofoafo  42106  naddcnff  42112  oaun3lem1  42124  oaun3lem2  42125  pr2cv  42299  brfvrcld2  42443  rfovcnvf1od  42755  ismnushort  43060  nzin  43077  pm10.14  43118  disjrnmpt2  43886  liminfvalxr  44499  etransclem38  44988  cfsetsnfsetf1  45769  tz6.12-afv2  45948  2elfz2melfz  46026  fz0addge0  46027  2ffzoeq  46036  icceuelpartlem  46103  icceuelpart  46104  ich2exprop  46139  sqrtpwpw2p  46206  fmtnoprmfac1lem  46232  fmtnoprmfac1  46233  lighneallem2  46274  divgcdoddALTV  46350  gbowpos  46427  gbowgt5  46430  gboge9  46432  nnsum3primesgbe  46460  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  isupwlkg  46515  rabsubmgmd  46561  resmgmhm2  46569  ismhm0  46575  mhmismgmhm  46576  isrnghmmul  46691  c0ghm  46710  rhmisrnghm  46723  subrngpropd  46747  rnghmsubcsetclem2  46874  rngcinv  46879  rngcinvALTV  46891  rhmsubcsetclem2  46920  rhmsubcrngclem2  46926  ringcinv  46930  ringcinvALTV  46954  srhmsubc  46974  srhmsubcALTV  46992  mapprop  47022  zlmodzxzadd  47034  domnmsuppn0  47045  mndpfsupp  47052  ply1mulgsumlem2  47068  lincsum  47110  lincsumcl  47112  lincscmcl  47113  isldepslvec2  47166  modn0mul  47206  digexp  47293  rrx2pnecoorneor  47401  rrx2pnedifcoorneorr  47403  rrx2xpref1o  47404  ehl2eudis0lt  47412  rrx2linest  47428  line2x  47440  itsclc0yqsollem2  47449  seppsepf  47561  thincn0eu  47652