Theorem anim12i 625

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 23	. 2 ⊢ ((𝜓 ∧ 𝜃) → (𝜓 ∧ 𝜃))
4	1, 2, 3	syl2an 608	1 ⊢ ((𝜑 ∧ 𝜒) → (𝜓 ∧ 𝜃))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  anim12ci  626  anim1i  627  anim2i  629  anifp  1088  cgsex2g  3502  cgsex4g  3503  spc2egv  3560  spc2ed  3562  uneqin  4242  2reu4lem  4486  2reu4  4487  disjpr2  4681  ssunieq  4911  iuneq1  4975  iuneq2  4978  copsex2t  5477  propeqop  5492  opthhausdorff  5502  opthhausdorff0  5503  iunopeqop  5506  iunopeqopOLD  5507  soeq2  5593  opbrop  5761  xpsspw  5798  coeq1  5845  coeq2  5846  cnveq  5861  dmeq  5895  sotri  6129  tz7.7  6390  funun  6586  fununfun  6588  fundif  6589  funprg  6594  funtp  6597  2elresin  6660  funssxp  6738  fssres  6748  f1cof1  6790  foun  6843  f1un  6845  resdif  6846  f1oco  6848  fvun  6975  elfvmptrab1w  7021  elfvmptrab1  7022  fvn0ssdmfun  7073  dff3  7099  exfo  7104  fprg  7156  ftpg  7157  f1ounsn  7276  weisoeq2  7362  oprabv  7476  ndmovdistr  7605  ndmovord  7606  brrpssg  7728  eldifpw  7769  iunpw  7772  epweon  7776  bropfvvvv  8089  f1o2ndf1  8119  poseq  8156  fvn0elsupp  8178  smores  8341  tz7.49  8434  tz7.49c  8435  oaord  8534  oeeulem  8589  nnaord  8607  brecop  8810  brecop2  8811  eroveu  8812  ecopovtrn  8820  ixpeq2  8911  undifixp  8934  sbthlem8  9085  sbthlem9  9086  unxpdom  9222  isinf  9228  f1opwfi  9316  fiin  9385  en2lp  9578  inf3lem3  9602  brttrcl  9685  tcmin  9711  djuexb  9907  alephfp  10104  kmlem16  10161  endjudisj  10164  cofsmo  10264  fin23lem28  10335  axdc3lem2  10446  ac6c4  10476  brdom3  10523  brdom5  10524  brdom4  10525  canthp1lem2  10649  finngch  10651  ordpipq  10938  adderpq  10952  mulerpq  10953  lterpq  10966  genpn0  10999  genpnnp  11001  addclprlem2  11013  addcmpblnr  11065  addsrpr  11071  mulsrpr  11072  addclsr  11079  addasssr  11084  distrsr  11087  0idsr  11093  1idsr  11094  00sr  11095  mulgt0sr  11101  axaddf  11141  axaddass  11152  axdistr  11154  cnegex  11402  recextlem2  11856  difgtsumgt  12568  zaddcl  12645  qaddcl  13000  qmulcl  13002  qreccl  13004  xmulgt0  13320  xrsupsslem  13344  xrinfmsslem  13345  supxrpnf  13355  iccss  13452  difreicc  13522  fzadd2  13599  fzsubel  13600  ssfzunsnext  13609  difelfznle  13682  2ffzeq  13689  nelfzo  13705  fzonmapblen  13749  ubmelfzo  13771  ubmelm1fzo  13804  elfznelfzo  13814  subfzo0  13834  adddivflid  13864  modaddid  13956  modifeq2int  13982  modaddmodup  13983  addmodlteq  13995  fsuppmapnn0fiub  14040  mulexp  14150  mulexpz  14151  leexp1a  14224  faclbnd  14339  hashunx  14435  hashgt23el  14474  wrdeq  14586  ccatcl  14624  swrdnd  14709  swrdnd0  14712  swrdsbslen  14719  swrdspsleq  14720  pfxccat1  14756  swrdswrdlem  14758  pfxccatin12lem2a  14781  swrdccatin2  14783  pfxccatin12lem2  14785  pfxccatin12  14787  swrdccat  14789  reuccatpfxs1  14801  repswswrd  14840  repswccat  14842  cshwidxn  14865  cshweqdif2  14875  2cshwcshw  14881  cshwcshid  14883  cshwcsh2id  14884  f1oun2prg  14973  s2eq2s1eq  14992  s3eqs2s1eq  14994  s3sndisj  15023  s3iunsndisj  15024  sqabsadd  15352  sqabssub  15353  abs2dif  15403  rexanuz  15416  o1of2  15683  o1rlimmul  15689  fsum2dlem  15839  isumltss  15920  fprodser  16021  fprodeq0  16047  fprod2dlem  16052  dvdscmulr  16359  dvdsmulcr  16360  summodnegmod  16361  difmod0  16362  dvds2ln  16364  dvdsflip  16392  divalglem9  16476  gcdcllem3  16576  gcdaddmlem  16599  sqgcd  16637  lcmcllem  16671  lcmabs  16680  lcmgcdlem  16681  lcmgcd  16682  lcmgcdeq  16687  lcmftp  16711  lcmfunsnlem2lem1  16713  qredeq  16732  cncongr1  16742  cncongr2  16743  isprm7  16784  hashgcdlem  16864  dvdsprmpweqle  16963  difsqpwdvds  16964  prmgaplem4  17131  cshwsidrepsw  17170  setsfun0  17249  setsstruct2  17251  xpsfrnel2  17635  isfunc  17938  tsrss  18662  chnpof1  18703  rabsubmgmd  18783  resmgmhm2  18791  mndpfsupp  18848  ismhm0  18871  mhmismgmhm  18872  mndissubm  18888  resmndismnd  18889  resmhm2  18903  submefmnd  18977  sursubmefmnd  18978  injsubmefmnd  18979  grpissubg  19236  gimco  19361  symg2bas  19486  pgrpsubgsymg  19502  symgextf  19510  fvcosymgeq  19522  gsmsymgreqlem1  19523  symgfixf1  19530  efgrelexlema  19842  gsum2dlem1  20063  gsum2dlem2  20064  dvdsr  20469  isrnghmmul  20549  c0ghm  20568  rhmisrnghm  20588  rimco  20624  subrngpropd  20696  subrgpropd  20736  rnghmsubcsetclem2  20760  rngcinv  20765  rhmsubcsetclem2  20789  rhmsubcrngclem2  20795  ringcinv  20799  srhmsubc  20808  isdrng3lem2  20881  islmhm2  21188  unichnlidl  21391  cmprmidlmcl  21504  psgnghm  21759  psgndiflemB  21779  frlmbas3  21955  frlmphl  21960  islindf4  22017  ressmpladd  22208  ressmplmul  22209  mplind  22250  mpomatmul  22632  mavmul0g  22739  1marepvsma1  22769  mdetdiag  22785  slesolvec  22865  cramerimplem2  22870  cramerimplem3  22871  cramerimp  22872  mat2pmatlin  22921  m2pmfzgsumcl  22934  monmatcollpw  22965  pmatcollpw3lem  22969  pmatcollpwscmatlem1  22975  chpmat1dlem  23021  chfacfisf  23040  chfacfisfcpmat  23041  chfacfpmmulgsum2  23051  tgcl  23155  uncld  23227  innei  23311  cnco  23452  uncmp  23589  txbas  23753  txbasval  23792  tx1stc  23836  fbun  24026  infil  24049  fbunfip  24055  filuni  24071  imaelfm  24137  txflf  24192  tsmsfbas  24314  tsmsxp  24341  blin2  24615  nmhmplusg  24943  qtopbaslem  24944  iccntr  25008  ncvspi  25344  ncvs1  25345  unmbl  25725  volfiniun  25735  mbfi1flimlem  25910  ply1idom  26311  logreclem  26956  relogbcxpb  26981  fsumvma2  27407  chpchtsum  27412  dchrelbas3  27431  dchrmulcl  27442  lgsmulsqcoprm  27536  gausslemma2dlem1a  27558  lgsquad2lem2  27578  dchrisum0fmul  27699  dchrisum0lem1  27709  ltsres  27855  nocvxminlem  27976  oldlim  28109  madebdayim  28110  madebdaylemlrcut  28121  readdscl  28721  remulscl  28724  ishpg  29070  brcgr  29279  brbtwn2  29284  axcontlem2  29344  uspgredg2v  29603  usgredg2v  29606  usgr2v1e2w  29631  nb3gr2nb  29763  cusgredg  29803  cplgr3v  29814  cusgrop  29817  rusgr1vtx  29967  iswlkg  29992  wlkeq  30012  wlk1walk  30017  uspgr2wlkeq2  30025  uspgr2wlkeqi  30026  cyclnumvtx  30178  crctcshwlkn0lem3  30190  crctcshwlkn0lem4  30191  crctcshwlkn0lem5  30192  wspthneq1eq2  30238  wwlksnextinj  30277  2wlkdlem7  30310  2wlkdlem8  30311  2pthon3v  30321  s3wwlks2on  30334  sps3wwlks2on  30335  elwwlks2  30347  elwspths2spth  30348  rusgrnumwwlks  30355  clwlkclwwlklem2a  30378  clwlkclwwlklem3  30381  clwlkclwwlkf1lem2  30385  clwlkclwwlkf1  30390  clwwlknonex2  30489  3wlkdlem3  30541  uhgr3cyclex  30562  cusconngr  30571  eupth0  30594  frgr3v  30655  1to3vfriswmgr  30660  4cycl2v2nb  30669  frgrnbnb  30673  frgrncvvdeq  30689  frgrwopreglem4a  30690  frgrwopreglem5a  30691  frgrwopreglem4  30695  frgrwopreglem5  30701  frgrhash2wsp  30712  numclwwlk1lem2foa  30734  numclwwlk2  30761  blocni  31186  hvsub4  31418  shscli  31698  shscom  31700  spanunsni  31960  spanpr  31961  5oalem2  32036  5oalem3  32037  5oalem5  32039  3oalem1  32043  hoscl  32126  hoadddi  32184  hoadddir  32185  hosub4  32194  lnophsi  32382  hmops  32401  hmopm  32402  adjadd  32474  leop2  32505  leopadd  32513  leopmuli  32514  pjclem4  32580  pj3si  32588  mdslmd1lem2  32707  mdslmd3i  32713  atomli  32763  atcvatlem  32766  chirredlem3  32773  chirredi  32775  atcvat3i  32777  mdsymlem1  32784  mdsymlem5  32788  cdjreui  32813  cdj3i  32822  addltmulALT  32827  hashxpe  33181  domnmuln0rd  33620  mndpluscn  34339  sxbrsigalem5  34702  probfinmeasbALTV  34843  bnj545  35307  bnj546  35308  bnj557  35313  bnj570  35317  bnj594  35324  bnj1001  35371  bnj1118  35396  txpconn  35737  cvmlift2lem10  35817  gonar  35900  lediv2aALT  36182  altopeq12  36467  altxpsspw  36482  funtransport  36536  neibastop1  36903  filnetlem3  36924  lukshef-ax2  36959  arg-ax  36960  nndivsub  37001  bj-nnfan  37412  bj-nnfor  37414  cgsex2gd  37814  copsex2b  37817  isbasisrelowllem1  38034  isbasisrelowllem2  38035  icoreclin  38036  relowlssretop  38042  rdgeqoa  38049  fvineqsnf1  38089  matunitlindflem1  38300  matunitlindflem2  38301  poimirlem4  38308  poimirlem26  38330  poimirlem29  38333  poimirlem30  38334  heicant  38339  mblfinlem1  38341  ismblfin  38345  itg2addnclem  38355  ftc1anclem6  38382  ftc1anclem7  38383  ftc1anclem8  38384  ftc1anc  38385  prdstotbnd  38478  heibor1lem  38493  isdrngo2  38642  divrngidl  38712  pridlc3  38757  eldisjdmqsim  39499  linepsubN  40559  pmapsub  40575  elpaddri  40609  paddasslem14  40640  pmapjoin  40659  dvhfvadd  41898  dvhvaddcomN  41903  bcle2d  42979  imacrhmcl  43321  rmxynorm  43678  monotoddzzfi  43702  acongtr  43738  mpaaeu  43910  oaltublim  44050  omord2lim  44060  cantnftermord  44080  dflim5  44089  omabs2  44092  tfsconcat0i  44105  ofoafo  44116  naddcnff  44122  oaun3lem1  44134  oaun3lem2  44135  pr2cv  44307  brfvrcld2  44451  rfovcnvf1od  44763  ismnushort  45044  nzin  45061  pm10.14  45102  disjrnmpt2  45939  liminfvalxr  46530  etransclem38  47019  cfsetsnfsetf1  47829  tz6.12-afv2  48010  2elfz2melfz  48088  fz0addge0  48089  2ffzoeq  48098  difltmodne  48118  modn0mul  48133  mod2addne  48140  icceuelpartlem  48217  icceuelpart  48218  ich2exprop  48253  sqrtpwpw2p  48323  fmtnoprmfac1lem  48349  fmtnoprmfac1  48350  lighneallem2  48391  divgcdoddALTV  48480  gbowpos  48557  gbowgt5  48560  gboge9  48562  nnsum3primesgbe  48590  bgoldbtbndlem2  48604  bgoldbtbndlem3  48605  isuspgrim  48694  clnbgrgrimlem  48731  clnbgrgrim  48732  isgrtri  48741  isubgr3stgrlem4  48767  grlimgrtri  48801  grlictr  48813  gpgedgvtx0  48859  gpgedg2iv  48865  gpg5nbgrvtx03star  48878  gpg5nbgr3star  48879  pgnbgreunbgrlem3  48916  pgnbgreunbgrlem6  48922  pgn4cyclex  48924  isupwlkg  48935  rngcinvALTV  49074  ringcinvALTV  49108  srhmsubcALTV  49123  mapprop  49159  zlmodzxzadd  49171  domnmsuppn0  49182  ply1mulgsumlem2  49200  lincsum  49242  lincsumcl  49244  lincscmcl  49245  isldepslvec2  49298  digexp  49420  rrx2pnecoorneor  49528  rrx2pnedifcoorneorr  49530  rrx2xpref1o  49531  ehl2eudis0lt  49539  rrx2linest  49555  line2x  49567  itsclc0yqsollem2  49576  seppsepf  49740  thincn0eu  50242  alseu-no-surprise  50649