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  3495  cgsex4g  3496  spc2egv  3553  spc2ed  3555  uneqin  4234  2reu4lem  4478  2reu4  4479  disjpr2  4670  ssunieq  4903  iuneq1  4967  iuneq2  4970  copsex2t  5463  propeqop  5478  opthhausdorff  5489  opthhausdorff0  5490  iunopeqop  5493  iunopeqopOLD  5494  soeq2  5580  opbrop  5748  xpsspw  5786  coeq1  5834  coeq2  5835  cnveq  5850  dmeq  5884  sotri  6120  tz7.7  6388  funun  6587  fununfun  6589  fundif  6590  funprg  6595  funtp  6598  2elresin  6661  funssxp  6739  fssres  6749  f1cof1  6791  foun  6844  f1un  6846  resdif  6847  f1oco  6849  fvun  6976  elfvmptrab1w  7022  elfvmptrab1  7023  fvn0ssdmfun  7075  dff3  7101  exfo  7106  fprg  7160  ftpg  7161  f1ounsn  7281  weisoeq2  7367  oprabv  7481  ndmovdistr  7611  ndmovord  7612  brrpssg  7742  eldifpw  7783  iunpw  7786  epweon  7790  bropfvvvv  8104  f1o2ndf1  8136  poseq  8178  fvn0elsupp  8201  smores  8364  tz7.49  8459  tz7.49c  8460  oaord  8559  oeeulem  8614  nnaord  8632  brecop  8835  brecop2  8836  eroveu  8837  ecopovtrn  8845  ixpeq2  8943  undifixp  8966  sbthlem8  9117  sbthlem9  9118  unxpdom  9254  isinf  9260  f1opwfi  9349  fiin  9418  en2lp  9611  inf3lem3  9635  brttrcl  9718  tcmin  9744  djuexb  9994  alephfp  10191  kmlem16  10248  endjudisj  10251  cofsmo  10351  fin23lem28  10422  axdc3lem2  10533  ac6c4  10563  brdom3  10611  brdom5  10612  brdom4  10613  canthp1lem2  10742  finngch  10744  ordpipq  11031  adderpq  11045  mulerpq  11046  lterpq  11059  genpn0  11092  genpnnp  11094  addclprlem2  11106  addcmpblnr  11158  addsrpr  11164  mulsrpr  11165  addclsr  11172  addasssr  11177  distrsr  11180  0idsr  11186  1idsr  11187  00sr  11188  mulgt0sr  11194  axaddf  11234  axaddass  11245  axdistr  11247  cnegex  11495  recextlem2  11951  difgtsumgt  12663  zaddcl  12740  qaddcl  13097  qmulcl  13099  qreccl  13101  xmulgt0  13417  xrsupsslem  13441  xrinfmsslem  13442  supxrpnf  13452  iccss  13549  difreicc  13619  fzadd2  13697  fzsubel  13698  ssfzunsnext  13707  difelfznle  13780  2ffzeq  13787  nelfzo  13803  fzonmapblen  13847  ubmelfzo  13869  ubmelm1fzo  13902  elfznelfzo  13912  subfzo0  13932  adddivflid  13962  modaddid  14054  modifeq2int  14080  modaddmodup  14081  addmodlteq  14093  fsuppmapnn0fiub  14138  mulexp  14248  mulexpz  14249  leexp1a  14322  faclbnd  14438  hashunx  14534  hashgt23el  14573  wrdeq  14685  ccatcl  14723  swrdnd  14809  swrdnd0  14812  swrdsbslen  14819  swrdspsleq  14820  pfxccat1  14856  swrdswrdlem  14858  pfxccatin12lem2a  14881  swrdccatin2  14883  pfxccatin12lem2  14885  pfxccatin12  14887  swrdccat  14889  reuccatpfxs1  14901  repswswrd  14940  repswccat  14942  cshwidxn  14965  cshweqdif2  14975  2cshwcshw  14981  cshwcshid  14983  cshwcsh2id  14984  f1oun2prg  15074  s2eq2s1eq  15093  s3eqs2s1eq  15095  s3sndisj  15126  s3iunsndisj  15127  sqabsadd  15455  sqabssub  15456  abs2dif  15506  rexanuz  15519  o1of2  15786  o1rlimmul  15792  fsum2dlem  15942  isumltss  16023  fprodser  16122  fprodeq0  16148  fprod2dlem  16153  dvdscmulr  16460  dvdsmulcr  16461  summodnegmod  16462  difmod0  16463  dvds2ln  16465  dvdsflip  16493  divalglem9  16577  gcdcllem3  16677  gcdaddmlem  16702  sqgcd  16742  lcmcllem  16777  lcmabs  16786  lcmgcdlem  16787  lcmgcd  16788  lcmgcdeq  16793  lcmftp  16817  lcmfunsnlem2lem1  16819  qredeq  16838  cncongr1  16848  cncongr2  16849  isprm7  16890  hashgcdlem  16971  dvdsprmpweqle  17070  difsqpwdvds  17071  prmgaplem4  17238  cshwsidrepsw  17277  setsfun0  17356  setsstruct2  17358  xpsfrnel2  17742  isfunc  18045  tsrss  18769  chnpof1  18810  rabsubmgmd  18899  resmgmhm2  18907  mndpfsupp  18967  ismhm0  18991  mhmismgmhm  18992  mndissubm  19008  resmndismnd  19009  resmhm2  19023  submefmnd  19097  sursubmefmnd  19098  injsubmefmnd  19099  grpissubg  19363  gimco  19488  symg2bas  19613  pgrpsubgsymg  19629  symgextf  19637  fvcosymgeq  19649  gsmsymgreqlem1  19650  symgfixf1  19657  efgrelexlema  19969  gsum2dlem1  20190  gsum2dlem2  20191  dvdsr  20598  isrnghmmul  20678  c0ghm  20697  rhmisrnghm  20717  rimco  20753  subrngpropd  20826  subrgpropd  20866  rnghmsubcsetclem2  20890  rngcinv  20895  rhmsubcsetclem2  20919  rhmsubcrngclem2  20925  ringcinv  20929  srhmsubc  20938  isdrng3lem2  21012  islmhm2  21319  unichnlidl  21522  cmprmidlmcl  21637  psgnghm  21892  psgndiflemB  21912  frlmbas3  22088  frlmphl  22093  islindf4  22150  ressmpladd  22343  ressmplmul  22344  mplind  22385  mpomatmul  22767  mavmul0g  22874  1marepvsma1  22904  mdetdiag  22920  matunitlindflem1  23000  matunitlindflem2  23001  slesolvec  23003  cramerimplem2  23008  cramerimplem3  23009  cramerimp  23010  mat2pmatlin  23059  m2pmfzgsumcl  23072  monmatcollpw  23103  pmatcollpw3lem  23107  pmatcollpwscmatlem1  23113  chpmat1dlem  23159  chfacfisf  23178  chfacfisfcpmat  23179  chfacfpmmulgsum2  23189  tgcl  23293  uncld  23365  innei  23449  cnco  23590  uncmp  23727  txbas  23892  txbasval  23931  tx1stc  23975  fbun  24165  infil  24188  fbunfip  24194  filuni  24210  imaelfm  24276  txflf  24331  tsmsfbas  24453  tsmsxp  24480  blin2  24754  nmhmplusg  25082  qtopbaslem  25083  iccntr  25147  ncvspi  25483  ncvs1  25484  unmbl  25864  volfiniun  25874  mbfi1flimlem  26049  ply1idom  26449  logreclem  27096  relogbcxpb  27121  fsumvma2  27547  chpchtsum  27552  dchrelbas3  27571  dchrmulcl  27582  lgsmulsqcoprm  27676  gausslemma2dlem1a  27698  lgsquad2lem2  27718  dchrisum0fmul  27839  dchrisum0lem1  27849  ltsres  28025  nocvxminlem  28146  oldlim  28279  madebdayim  28280  madebdaylemlrcut  28291  readdscl  28891  remulscl  28894  ishpg  29243  brcgr  29484  brbtwn2  29489  axcontlem2  29549  uspgredg2v  29811  usgredg2v  29814  usgr2v1e2w  29839  nb3gr2nb  29971  cusgredg  30011  cplgr3v  30022  cusgrop  30025  rusgr1vtx  30175  iswlkg  30200  wlkeq  30220  wlk1walk  30225  uspgr2wlkeq2  30233  uspgr2wlkeqi  30234  cyclnumvtx  30394  crctcshwlkn0lem3  30407  crctcshwlkn0lem4  30408  crctcshwlkn0lem5  30409  wspthneq1eq2  30455  wwlksnextinj  30494  2wlkdlem7  30527  2wlkdlem8  30528  2pthon3v  30538  s3wwlks2on  30551  sps3wwlks2on  30552  elwwlks2  30564  elwspths2spth  30565  rusgrnumwwlks  30572  clwlkclwwlklem2a  30595  clwlkclwwlklem3  30598  clwlkclwwlkf1lem2  30602  clwlkclwwlkf1  30607  clwwlknonex2  30706  3wlkdlem3  30768  uhgr3cyclex  30789  cusconngr  30798  eupth0  30821  frgr3v  30882  1to3vfriswmgr  30887  4cycl2v2nb  30896  frgrnbnb  30900  frgrncvvdeq  30916  frgrwopreglem4a  30917  frgrwopreglem5a  30918  frgrwopreglem4  30922  frgrwopreglem5  30928  frgrhash2wsp  30939  numclwwlk1lem2foa  30961  numclwwlk2  30988  blocni  31413  hvsub4  31645  shscli  31925  shscom  31927  spanunsni  32187  spanpr  32188  5oalem2  32263  5oalem3  32264  5oalem5  32266  3oalem1  32270  hoscl  32353  hoadddi  32411  hoadddir  32412  hosub4  32421  lnophsi  32609  hmops  32628  hmopm  32629  adjadd  32701  leop2  32732  leopadd  32740  leopmuli  32741  pjclem4  32807  pj3si  32815  mdslmd1lem2  32934  mdslmd3i  32940  atomli  32990  atcvatlem  32993  chirredlem3  33000  chirredi  33002  atcvat3i  33004  mdsymlem1  33011  mdsymlem5  33015  cdjreui  33040  cdj3i  33049  addltmulALT  33096  hashxpe  33446  domnmuln0rd  33885  mndpluscn  34605  sxbrsigalem5  34967  probfinmeasbALTV  35108  bnj545  35572  bnj546  35573  bnj557  35578  bnj570  35582  bnj594  35589  bnj1001  35636  bnj1118  35661  j0ltaleph  35948  txpconn  36084  cvmlift2lem10  36164  gonar  36247  lediv2aALT  36529  altopeq12  36820  altxpsspw  36835  funtransport  36889  neibastop1  37240  filnetlem3  37261  lukshef-ax2  37296  arg-ax  37297  nndivsub  37338  bj-nnfan  37749  bj-nnfor  37751  cgsex2gd  38152  copsex2b  38155  isbasisrelowllem1  38372  isbasisrelowllem2  38373  icoreclin  38374  relowlssretop  38380  rdgeqoa  38387  fvineqsnf1  38427  poimirlem4  38636  poimirlem26  38658  poimirlem29  38661  poimirlem30  38662  heicant  38667  mblfinlem1  38669  ismblfin  38673  itg2addnclem  38683  ftc1anclem6  38710  ftc1anclem7  38711  ftc1anclem8  38712  ftc1anc  38713  impprop  38738  prdstotbnd  38822  heibor1lem  38837  isdrngo2  38986  divrngidl  39056  pridlc3  39101  eldisjdmqsim  39843  linepsubN  40903  pmapsub  40919  elpaddri  40953  paddasslem14  40984  pmapjoin  41003  dvhfvadd  42242  dvhvaddcomN  42247  bcle2d  43323  imacrhmcl  43675  rmxynorm  44019  monotoddzzfi  44043  acongtr  44079  mpaaeu  44246  oaltublim  44386  omord2lim  44396  cantnftermord  44416  dflim5  44425  omabs2  44428  tfsconcat0i  44441  ofoafo  44452  naddcnff  44458  oaun3lem1  44470  oaun3lem2  44471  pr2cv  44643  brfvrcld2  44786  rfovcnvf1od  45098  ismnushort  45379  nzin  45396  pm10.14  45437  disjrnmpt2  46297  liminfvalxr  46887  etransclem38  47376  wrddin  47990  cfsetsnfsetf1  48223  tz6.12-afv2  48404  2elfz2melfz  48482  fz0addge0  48483  2ffzoeq  48492  difltmodne  48512  modn0mul  48527  mod2addne  48534  icceuelpartlem  48611  icceuelpart  48612  ich2exprop  48647  sqrtpwpw2p  48717  fmtnoprmfac1lem  48743  fmtnoprmfac1  48744  lighneallem2  48785  divgcdoddALTV  48874  gbowpos  48951  gbowgt5  48954  gboge9  48956  nnsum3primesgbe  48984  bgoldbtbndlem2  48998  bgoldbtbndlem3  48999  isuspgrim  49088  clnbgrgrimlem  49125  clnbgrgrim  49126  isgrtri  49135  isubgr3stgrlem4  49161  grlimgrtri  49195  grlictr  49207  gpgedgvtx0  49253  gpgedg2iv  49259  gpg5nbgrvtx03star  49272  gpg5nbgr3star  49273  pgnbgreunbgrlem3  49310  pgnbgreunbgrlem6  49316  pgn4cyclex  49318  isupwlkg  49329  rngcinvALTV  49467  ringcinvALTV  49501  srhmsubcALTV  49516  mapprop  49552  zlmodzxzadd  49564  domnmsuppn0  49575  ply1mulgsumlem2  49593  lincsum  49635  lincsumcl  49637  lincscmcl  49638  isldepslvec2  49691  digexp  49813  rrx2pnecoorneor  49922  rrx2pnedifcoorneorr  49924  ehl2eudis0lt  49933  rrx2linest  49948  itsclc0yqsollem2  49969  seppsepf  50137  thincn0eu  50660  alseu-no-surprise  51103