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  3499  cgsex4g  3500  spc2egv  3557  spc2ed  3559  uneqin  4237  2reu4lem  4482  2reu4  4483  disjpr2  4674  ssunieq  4907  iuneq1  4971  iuneq2  4974  copsex2t  5469  propeqop  5484  opthhausdorff  5495  opthhausdorff0  5496  iunopeqop  5499  iunopeqopOLD  5500  soeq2  5586  opbrop  5755  xpsspw  5794  coeq1  5844  coeq2  5845  cnveq  5861  dmeq  5895  sotri  6137  tz7.7  6412  funun  6612  fununfunOLD  6615  fundifOLD  6617  funprg  6622  funtp  6625  2elresin  6688  funssxp  6766  fssres  6776  f1cof1  6818  foun  6871  f1un  6873  resdif  6874  f1oco  6876  fvun  7004  elfvmptrab1w  7050  elfvmptrab1  7051  fvn0ssdmfun  7104  dff3  7130  exfo  7135  fprg  7189  ftpg  7190  f1ounsn  7309  weisoeq2  7395  oprabv  7509  ndmovdistr  7640  ndmovord  7641  brrpssg  7771  eldifpw  7812  iunpw  7815  epweon  7819  bropfvvvv  8136  f1o2ndf1  8168  poseq  8210  fvn0elsupp  8233  smores  8396  tz7.49  8491  tz7.49c  8492  oaord  8591  oeeulem  8646  nnaord  8664  brecop  8867  brecop2  8868  eroveu  8869  ecopovtrn  8877  ixpeq2  8975  undifixp  8998  sbthlem8  9149  sbthlem9  9150  unxpdom  9286  isinf  9292  f1opwfi  9381  fiin  9449  en2lp  9642  inf3lem3  9666  brttrcl  9749  tcmin  9775  djuexb  10025  alephfp  10224  kmlem16  10281  endjudisj  10284  cofsmo  10384  fin23lem28  10455  axdc3lem2  10566  ac6c4  10596  brdom3  10644  brdom5  10645  brdom4  10646  canthp1lem2  10775  finngch  10777  ordpipq  11064  adderpq  11078  mulerpq  11079  lterpq  11092  genpn0  11125  genpnnp  11127  addclprlem2  11139  addcmpblnr  11191  addsrpr  11197  mulsrpr  11198  addclsr  11205  addasssr  11210  distrsr  11213  0idsr  11219  1idsr  11220  00sr  11221  mulgt0sr  11227  axaddf  11267  axaddass  11278  axdistr  11280  cnegex  11528  recextlem2  11985  difgtsumgt  12697  zaddcl  12774  qaddcl  13131  qmulcl  13133  qreccl  13135  xmulgt0  13451  xrsupsslem  13475  xrinfmsslem  13476  supxrpnf  13486  iccss  13583  difreicc  13653  fzadd2  13731  fzsubel  13732  ssfzunsnext  13741  difelfznle  13814  2ffzeq  13821  nelfzo  13837  fzonmapblen  13881  ubmelfzo  13903  ubmelm1fzo  13936  elfznelfzo  13946  subfzo0  13966  adddivflid  13996  modaddid  14088  modifeq2int  14114  modaddmodup  14115  addmodlteq  14127  fsuppmapnn0fiub  14172  mulexp  14282  mulexpz  14283  leexp1a  14356  faclbnd  14473  hashunx  14569  hashgt23el  14608  wrdeq  14720  ccatcl  14758  swrdnd  14844  swrdnd0  14847  swrdsbslen  14854  swrdspsleq  14855  pfxccat1  14891  swrdswrdlem  14893  pfxccatin12lem2a  14916  swrdccatin2  14918  pfxccatin12lem2  14920  pfxccatin12  14922  swrdccat  14924  reuccatpfxs1  14936  repswswrd  14975  repswccat  14977  cshwidxn  15000  cshweqdif2  15010  2cshwcshw  15016  cshwcshid  15018  cshwcsh2id  15019  f1oun2prg  15109  s2eq2s1eq  15128  s3eqs2s1eq  15130  s3sndisj  15161  s3iunsndisj  15162  sqabsadd  15490  sqabssub  15491  abs2dif  15541  rexanuz  15554  o1of2  15821  o1rlimmul  15827  fsum2dlem  15977  isumltss  16058  fprodser  16157  fprodeq0  16183  fprod2dlem  16188  dvdscmulr  16495  dvdsmulcr  16496  summodnegmod  16497  difmod0  16498  dvds2ln  16500  dvdsflip  16528  divalglem9  16612  gcdcllem3  16712  gcdaddmlem  16737  sqgcd  16777  lcmcllem  16812  lcmabs  16821  lcmgcdlem  16822  lcmgcd  16823  lcmgcdeq  16828  lcmftp  16852  lcmfunsnlem2lem1  16854  qredeq  16873  cncongr1  16883  cncongr2  16884  isprm7  16925  hashgcdlem  17006  dvdsprmpweqle  17105  difsqpwdvds  17106  prmgaplem4  17273  cshwsidrepsw  17312  setsfun0  17391  setsstruct2  17393  xpsfrnel2  17777  isfunc  18080  tsrss  18804  chnpof1  18845  rabsubmgmd  18934  resmgmhm2  18942  mndpfsupp  19002  ismhm0  19026  mhmismgmhm  19027  mndissubm  19043  resmndismnd  19044  resmhm2  19058  submefmnd  19132  sursubmefmnd  19133  injsubmefmnd  19134  grpissubg  19398  gimco  19523  symg2bas  19649  pgrpsubgsymg  19665  symgextf  19673  fvcosymgeq  19685  gsmsymgreqlem1  19686  symgfixf1  19693  efgrelexlema  20005  gsum2dlem1  20226  gsum2dlem2  20227  dvdsr  20634  isrnghmmul  20714  c0ghm  20733  rhmisrnghm  20753  rimco  20789  subrngpropd  20862  subrgpropd  20902  rnghmsubcsetclem2  20926  rngcinv  20931  rhmsubcsetclem2  20955  rhmsubcrngclem2  20961  ringcinv  20965  srhmsubc  20974  isdrng3lem2  21048  islmhm2  21355  unichnlidl  21558  cmprmidlmcl  21673  psgnghm  21930  psgndiflemB  21950  frlmbas3  22126  frlmphl  22131  islindf4  22188  ressmpladd  22381  ressmplmul  22382  mplind  22423  mpomatmul  22805  mavmul0g  22912  1marepvsma1  22942  mdetdiag  22958  matunitlindflem1  23038  matunitlindflem2  23039  slesolvec  23041  cramerimplem2  23046  cramerimplem3  23047  cramerimp  23048  mat2pmatlin  23097  m2pmfzgsumcl  23110  monmatcollpw  23141  pmatcollpw3lem  23145  pmatcollpwscmatlem1  23151  chpmat1dlem  23197  chfacfisf  23216  chfacfisfcpmat  23217  chfacfpmmulgsum2  23227  tgcl  23331  uncld  23403  innei  23487  cnco  23628  uncmp  23765  txbas  23930  txbasval  23969  tx1stc  24013  fbun  24203  infil  24226  fbunfip  24232  filuni  24248  imaelfm  24314  txflf  24369  tsmsfbas  24491  tsmsxp  24518  blin2  24792  nmhmplusg  25120  qtopbaslem  25121  iccntr  25185  ncvspi  25521  ncvs1  25522  unmbl  25902  volfiniun  25912  mbfi1flimlem  26087  ply1idom  26487  logreclem  27136  relogbcxpb  27161  fsumvma2  27587  chpchtsum  27592  dchrelbas3  27611  dchrmulcl  27622  lgsmulsqcoprm  27716  gausslemma2dlem1a  27738  lgsquad2lem2  27758  dchrisum0fmul  27879  dchrisum0lem1  27889  ltsres  28065  nocvxminlem  28186  oldlim  28319  madebdayim  28320  madebdaylemlrcut  28331  readdscl  28931  remulscl  28934  ishpg  29283  brcgr  29524  brbtwn2  29529  axcontlem2  29589  uspgredg2v  29851  usgredg2v  29854  usgr2v1e2w  29879  nb3gr2nb  30011  cusgredg  30051  cplgr3v  30062  cusgrop  30065  rusgr1vtx  30215  iswlkg  30240  wlkeq  30260  wlk1walk  30265  uspgr2wlkeq2  30273  uspgr2wlkeqi  30274  cyclnumvtx  30434  crctcshwlkn0lem3  30447  crctcshwlkn0lem4  30448  crctcshwlkn0lem5  30449  wspthneq1eq2  30495  wwlksnextinj  30534  2wlkdlem7  30567  2wlkdlem8  30568  2pthon3v  30578  s3wwlks2on  30591  sps3wwlks2on  30592  elwwlks2  30604  elwspths2spth  30605  rusgrnumwwlks  30612  clwlkclwwlklem2a  30635  clwlkclwwlklem3  30638  clwlkclwwlkf1lem2  30642  clwlkclwwlkf1  30647  clwwlknonex2  30746  3wlkdlem3  30808  uhgr3cyclex  30829  cusconngr  30838  eupth0  30861  frgr3v  30922  1to3vfriswmgr  30927  4cycl2v2nb  30936  frgrnbnb  30940  frgrncvvdeq  30956  frgrwopreglem4a  30957  frgrwopreglem5a  30958  frgrwopreglem4  30962  frgrwopreglem5  30968  frgrhash2wsp  30979  numclwwlk1lem2foa  31001  numclwwlk2  31028  blocni  31453  hvsub4  31685  shscli  31965  shscom  31967  spanunsni  32227  spanpr  32228  5oalem2  32303  5oalem3  32304  5oalem5  32306  3oalem1  32310  hoscl  32393  hoadddi  32451  hoadddir  32452  hosub4  32461  lnophsi  32649  hmops  32668  hmopm  32669  adjadd  32741  leop2  32772  leopadd  32780  leopmuli  32781  pjclem4  32847  pj3si  32855  mdslmd1lem2  32974  mdslmd3i  32980  atomli  33030  atcvatlem  33033  chirredlem3  33040  chirredi  33042  atcvat3i  33044  mdsymlem1  33051  mdsymlem5  33055  cdjreui  33080  cdj3i  33089  addltmulALT  33136  hashxpe  33485  domnmuln0rd  33927  mndpluscn  34662  sxbrsigalem5  35024  probfinmeasbALTV  35165  bnj545  35629  bnj546  35630  bnj557  35635  bnj570  35639  bnj594  35646  bnj1001  35693  bnj1118  35718  j0ltaleph  36042  txpconn  36198  cvmlift2lem10  36278  gonar  36361  lediv2aALT  36643  altopeq12  36935  altxpsspw  36950  funtransport  37004  neibastop1  37355  filnetlem3  37376  lukshef-ax2  37411  arg-ax  37412  nndivsub  37453  bj-nnfan  37864  bj-nnfor  37866  cgsex2gd  38322  copsex2b  38325  isbasisrelowllem1  38539  isbasisrelowllem2  38540  icoreclin  38541  relowlssretop  38547  rdgeqoa  38554  fvineqsnf1  38594  poimirlem4  38803  poimirlem26  38825  poimirlem29  38828  poimirlem30  38829  heicant  38834  mblfinlem1  38836  ismblfin  38840  itg2addnclem  38850  ftc1anclem6  38877  ftc1anclem7  38878  ftc1anclem8  38879  ftc1anc  38880  impprop  38905  prdstotbnd  38987  heibor1lem  39002  isdrngo2  39151  divrngidl  39221  pridlc3  39266  eldisjdmqsim  40008  linepsubN  41068  pmapsub  41084  elpaddri  41118  paddasslem14  41149  pmapjoin  41168  dvhfvadd  42407  dvhvaddcomN  42412  bcle2d  43488  imacrhmcl  43841  rmxynorm  44185  monotoddzzfi  44209  acongtr  44245  mpaaeu  44411  oaltublim  44547  omord2lim  44557  cantnftermord  44577  dflim5  44586  omabs2  44589  tfsconcat0i  44602  ofoafo  44613  naddcnff  44619  oaun3lem1  44631  oaun3lem2  44632  pr2cv  44804  brfvrcld2  44947  rfovcnvf1od  45259  ismnushort  45540  nzin  45557  pm10.14  45598  relpropg  46176  disjrnmpt2  46470  liminfvalxr  47060  etransclem38  47549  wrddin  48163  cfsetsnfsetf1  48396  tz6.12-afv2  48577  2elfz2melfz  48655  fz0addge0  48656  2ffzoeq  48665  difltmodne  48685  modn0mul  48700  mod2addne  48707  icceuelpartlem  48784  icceuelpart  48785  ich2exprop  48820  sqrtpwpw2p  48890  fmtnoprmfac1lem  48916  fmtnoprmfac1  48917  lighneallem2  48958  divgcdoddALTV  49047  gbowpos  49124  gbowgt5  49127  gboge9  49129  nnsum3primesgbe  49157  bgoldbtbndlem2  49171  bgoldbtbndlem3  49172  isuspgrim  49261  clnbgrgrimlem  49298  clnbgrgrim  49299  isgrtri  49308  isubgr3stgrlem4  49334  grlimgrtri  49368  grlictr  49380  gpgedgvtx0  49426  gpgedg2iv  49432  gpg5nbgrvtx03star  49445  gpg5nbgr3star  49446  pgnbgreunbgrlem3  49483  pgnbgreunbgrlem6  49489  pgn4cyclex  49491  isupwlkg  49502  rngcinvALTV  49640  ringcinvALTV  49674  srhmsubcALTV  49689  laznegcl  49730  mapprop  49783  zlmodzxzadd  49795  domnmsuppn0  49806  ply1mulgsumlem2  49824  lincsum  49866  lincsumcl  49868  lincscmcl  49869  isldepslvec2  49922  digexp  50044  rrx2pnecoorneor  50153  rrx2pnedifcoorneorr  50155  ehl2eudis0lt  50164  rrx2linest  50179  itsclc0yqsollem2  50200  seppsepf  50368  thincn0eu  50891  alseu-no-surprise  51356