Theorem anim12i 624

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

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

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 401

This theorem is used by:  anim12ci  625  anim1i  626  anim2i  628  anifp  1088  cgsex2g  3500  cgsex4g  3501  spc2egv  3558  spc2ed  3560  uneqin  4242  2reu4lem  4484  2reu4  4485  disjpr2  4679  ssunieq  4909  iuneq1  4973  iuneq2  4976  copsex2t  5475  propeqop  5490  opthhausdorff  5500  opthhausdorff0  5501  iunopeqop  5504  iunopeqopOLD  5505  soeq2  5591  opbrop  5759  xpsspw  5796  coeq1  5843  coeq2  5844  cnveq  5859  dmeq  5893  sotri  6127  tz7.7  6386  funun  6582  fununfun  6584  fundif  6585  funprg  6590  funtp  6593  2elresin  6656  funssxp  6734  fssres  6744  f1cof1  6786  foun  6839  f1un  6841  resdif  6842  f1oco  6844  fvun  6971  elfvmptrab1w  7017  elfvmptrab1  7018  fvn0ssdmfun  7069  dff3  7095  exfo  7100  fprg  7152  ftpg  7153  f1ounsn  7270  weisoeq2  7354  oprabv  7470  ndmovdistr  7599  ndmovord  7600  brrpssg  7722  eldifpw  7763  iunpw  7766  epweon  7770  bropfvvvv  8083  f1o2ndf1  8113  poseq  8150  fvn0elsupp  8172  smores  8335  tz7.49  8428  tz7.49c  8429  oaord  8528  oeeulem  8583  nnaord  8601  brecop  8804  brecop2  8805  eroveu  8806  ecopovtrn  8814  ixpeq2  8905  undifixp  8928  sbthlem8  9078  sbthlem9  9079  unxpdom  9215  isinf  9221  f1opwfi  9309  fiin  9378  en2lp  9571  inf3lem3  9595  brttrcl  9678  tcmin  9704  djuexb  9900  alephfp  10097  kmlem16  10154  endjudisj  10157  cofsmo  10257  fin23lem28  10328  axdc3lem2  10439  ac6c4  10469  brdom3  10516  brdom5  10517  brdom4  10518  canthp1lem2  10642  finngch  10644  ordpipq  10931  adderpq  10945  mulerpq  10946  lterpq  10959  genpn0  10992  genpnnp  10994  addclprlem2  11006  addcmpblnr  11058  addsrpr  11064  mulsrpr  11065  addclsr  11072  addasssr  11077  distrsr  11080  0idsr  11086  1idsr  11087  00sr  11088  mulgt0sr  11094  axaddf  11134  axaddass  11145  axdistr  11147  cnegex  11395  recextlem2  11849  difgtsumgt  12561  zaddcl  12638  qaddcl  12993  qmulcl  12995  qreccl  12997  xmulgt0  13313  xrsupsslem  13337  xrinfmsslem  13338  supxrpnf  13348  iccss  13445  difreicc  13515  fzadd2  13592  fzsubel  13593  ssfzunsnext  13602  difelfznle  13675  2ffzeq  13682  nelfzo  13698  fzonmapblen  13742  ubmelfzo  13764  ubmelm1fzo  13797  elfznelfzo  13807  subfzo0  13826  adddivflid  13856  modaddid  13948  modifeq2int  13974  modaddmodup  13975  addmodlteq  13987  fsuppmapnn0fiub  14032  mulexp  14142  mulexpz  14143  leexp1a  14216  faclbnd  14331  hashunx  14427  hashgt23el  14466  wrdeq  14578  ccatcl  14616  swrdnd  14697  swrdnd0  14700  swrdsbslen  14707  swrdspsleq  14708  pfxccat1  14744  swrdswrdlem  14746  pfxccatin12lem2a  14769  swrdccatin2  14771  pfxccatin12lem2  14773  pfxccatin12  14775  swrdccat  14777  reuccatpfxs1  14789  repswswrd  14826  repswccat  14828  cshwidxn  14851  cshweqdif2  14861  2cshwcshw  14867  cshwcshid  14869  cshwcsh2id  14870  f1oun2prg  14959  s2eq2s1eq  14978  s3eqs2s1eq  14980  s3sndisj  15009  s3iunsndisj  15010  sqabsadd  15338  sqabssub  15339  abs2dif  15389  rexanuz  15402  o1of2  15669  o1rlimmul  15675  fsum2dlem  15826  isumltss  15907  fprodser  16008  fprodeq0  16034  fprod2dlem  16039  dvdscmulr  16346  dvdsmulcr  16347  summodnegmod  16348  difmod0  16349  dvds2ln  16351  dvdsflip  16379  divalglem9  16463  gcdcllem3  16563  gcdaddmlem  16586  sqgcd  16624  lcmcllem  16658  lcmabs  16667  lcmgcdlem  16668  lcmgcd  16669  lcmgcdeq  16674  lcmftp  16698  lcmfunsnlem2lem1  16700  qredeq  16719  cncongr1  16729  cncongr2  16730  isprm7  16771  hashgcdlem  16851  dvdsprmpweqle  16950  difsqpwdvds  16951  prmgaplem4  17118  cshwsidrepsw  17157  setsfun0  17236  setsstruct2  17238  xpsfrnel2  17622  isfunc  17925  tsrss  18649  chnpof1  18690  rabsubmgmd  18766  resmgmhm2  18774  mndpfsupp  18829  ismhm0  18852  mhmismgmhm  18853  mndissubm  18869  resmndismnd  18870  resmhm2  18884  submefmnd  18958  sursubmefmnd  18959  injsubmefmnd  18960  grpissubg  19217  gimco  19342  symg2bas  19467  pgrpsubgsymg  19483  symgextf  19491  fvcosymgeq  19503  gsmsymgreqlem1  19504  symgfixf1  19511  efgrelexlema  19823  gsum2dlem1  20044  gsum2dlem2  20045  dvdsr  20449  isrnghmmul  20529  c0ghm  20548  rhmisrnghm  20568  rimco  20604  subrngpropd  20676  subrgpropd  20716  rnghmsubcsetclem2  20740  rngcinv  20745  rhmsubcsetclem2  20769  rhmsubcrngclem2  20775  ringcinv  20779  srhmsubc  20788  isdrng3lem2  20861  islmhm2  21168  unichnlidl  21371  cmprmidlmcl  21484  psgnghm  21739  psgndiflemB  21759  frlmbas3  21935  frlmphl  21940  islindf4  21997  ressmpladd  22188  ressmplmul  22189  mplind  22230  mpomatmul  22612  mavmul0g  22719  1marepvsma1  22749  mdetdiag  22765  slesolvec  22845  cramerimplem2  22850  cramerimplem3  22851  cramerimp  22852  mat2pmatlin  22901  m2pmfzgsumcl  22914  monmatcollpw  22945  pmatcollpw3lem  22949  pmatcollpwscmatlem1  22955  chpmat1dlem  23001  chfacfisf  23020  chfacfisfcpmat  23021  chfacfpmmulgsum2  23031  tgcl  23135  uncld  23207  innei  23291  cnco  23432  uncmp  23569  txbas  23733  txbasval  23772  tx1stc  23816  fbun  24006  infil  24029  fbunfip  24035  filuni  24051  imaelfm  24117  txflf  24172  tsmsfbas  24294  tsmsxp  24321  blin2  24595  nmhmplusg  24923  qtopbaslem  24924  iccntr  24988  ncvspi  25324  ncvs1  25325  unmbl  25705  volfiniun  25715  mbfi1flimlem  25890  ply1idom  26291  logreclem  26936  relogbcxpb  26961  fsumvma2  27387  chpchtsum  27392  dchrelbas3  27411  dchrmulcl  27422  lgsmulsqcoprm  27516  gausslemma2dlem1a  27538  lgsquad2lem2  27558  dchrisum0fmul  27679  dchrisum0lem1  27689  ltsres  27835  nocvxminlem  27956  oldlim  28089  madebdayim  28090  madebdaylemlrcut  28101  readdscl  28701  remulscl  28704  ishpg  29050  brcgr  29259  brbtwn2  29264  axcontlem2  29324  uspgredg2v  29583  usgredg2v  29586  usgr2v1e2w  29611  nb3gr2nb  29743  cusgredg  29783  cplgr3v  29794  cusgrop  29797  rusgr1vtx  29947  iswlkg  29972  wlkeq  29992  wlk1walk  29997  uspgr2wlkeq2  30005  uspgr2wlkeqi  30006  cyclnumvtx  30158  crctcshwlkn0lem3  30170  crctcshwlkn0lem4  30171  crctcshwlkn0lem5  30172  wspthneq1eq2  30218  wwlksnextinj  30257  2wlkdlem7  30290  2wlkdlem8  30291  2pthon3v  30301  s3wwlks2on  30314  sps3wwlks2on  30315  elwwlks2  30327  elwspths2spth  30328  rusgrnumwwlks  30335  clwlkclwwlklem2a  30358  clwlkclwwlklem3  30361  clwlkclwwlkf1lem2  30365  clwlkclwwlkf1  30370  clwwlknonex2  30469  3wlkdlem3  30521  uhgr3cyclex  30542  cusconngr  30551  eupth0  30574  frgr3v  30635  1to3vfriswmgr  30640  4cycl2v2nb  30649  frgrnbnb  30653  frgrncvvdeq  30669  frgrwopreglem4a  30670  frgrwopreglem5a  30671  frgrwopreglem4  30675  frgrwopreglem5  30681  frgrhash2wsp  30692  numclwwlk1lem2foa  30714  numclwwlk2  30741  blocni  31166  hvsub4  31398  shscli  31678  shscom  31680  spanunsni  31940  spanpr  31941  5oalem2  32016  5oalem3  32017  5oalem5  32019  3oalem1  32023  hoscl  32106  hoadddi  32164  hoadddir  32165  hosub4  32174  lnophsi  32362  hmops  32381  hmopm  32382  adjadd  32454  leop2  32485  leopadd  32493  leopmuli  32494  pjclem4  32560  pj3si  32568  mdslmd1lem2  32687  mdslmd3i  32693  atomli  32743  atcvatlem  32746  chirredlem3  32753  chirredi  32755  atcvat3i  32757  mdsymlem1  32764  mdsymlem5  32768  cdjreui  32793  cdj3i  32802  addltmulALT  32807  hashxpe  33161  domnmuln0rd  33606  mndpluscn  34325  sxbrsigalem5  34687  probfinmeasbALTV  34828  bnj545  35292  bnj546  35293  bnj557  35298  bnj570  35302  bnj594  35309  bnj1001  35356  bnj1118  35381  txpconn  35732  cvmlift2lem10  35812  gonar  35895  lediv2aALT  36177  altopeq12  36462  altxpsspw  36477  funtransport  36531  neibastop1  36898  filnetlem3  36919  lukshef-ax2  36954  arg-ax  36955  nndivsub  36996  bj-nnfan  37407  bj-nnfor  37409  cgsex2gd  37809  copsex2b  37812  isbasisrelowllem1  38029  isbasisrelowllem2  38030  icoreclin  38031  relowlssretop  38037  rdgeqoa  38044  fvineqsnf1  38084  matunitlindflem1  38295  matunitlindflem2  38296  poimirlem4  38303  poimirlem26  38325  poimirlem29  38328  poimirlem30  38329  heicant  38334  mblfinlem1  38336  ismblfin  38340  itg2addnclem  38350  ftc1anclem6  38377  ftc1anclem7  38378  ftc1anclem8  38379  ftc1anc  38380  prdstotbnd  38473  heibor1lem  38488  isdrngo2  38637  divrngidl  38707  pridlc3  38752  eldisjdmqsim  39494  linepsubN  40554  pmapsub  40570  elpaddri  40604  paddasslem14  40635  pmapjoin  40654  dvhfvadd  41893  dvhvaddcomN  41898  bcle2d  42974  imacrhmcl  43316  rmxynorm  43673  monotoddzzfi  43697  acongtr  43733  mpaaeu  43905  oaltublim  44045  omord2lim  44055  cantnftermord  44075  dflim5  44084  omabs2  44087  tfsconcat0i  44100  ofoafo  44111  naddcnff  44117  oaun3lem1  44129  oaun3lem2  44130  pr2cv  44302  brfvrcld2  44446  rfovcnvf1od  44758  ismnushort  45039  nzin  45056  pm10.14  45097  disjrnmpt2  45934  liminfvalxr  46525  etransclem38  47014  cfsetsnfsetf1  47824  tz6.12-afv2  48005  2elfz2melfz  48083  fz0addge0  48084  2ffzoeq  48093  difltmodne  48113  modn0mul  48128  mod2addne  48135  icceuelpartlem  48212  icceuelpart  48213  ich2exprop  48248  sqrtpwpw2p  48318  fmtnoprmfac1lem  48344  fmtnoprmfac1  48345  lighneallem2  48386  divgcdoddALTV  48475  gbowpos  48552  gbowgt5  48555  gboge9  48557  nnsum3primesgbe  48585  bgoldbtbndlem2  48599  bgoldbtbndlem3  48600  isuspgrim  48689  clnbgrgrimlem  48726  clnbgrgrim  48727  isgrtri  48736  isubgr3stgrlem4  48762  grlimgrtri  48796  grlictr  48808  gpgedgvtx0  48854  gpgedg2iv  48860  gpg5nbgrvtx03star  48873  gpg5nbgr3star  48874  pgnbgreunbgrlem3  48911  pgnbgreunbgrlem6  48917  pgn4cyclex  48919  isupwlkg  48930  rngcinvALTV  49069  ringcinvALTV  49103  srhmsubcALTV  49118  mapprop  49154  zlmodzxzadd  49166  domnmsuppn0  49177  ply1mulgsumlem2  49195  lincsum  49237  lincsumcl  49239  lincscmcl  49240  isldepslvec2  49293  digexp  49415  rrx2pnecoorneor  49523  rrx2pnedifcoorneorr  49525  rrx2xpref1o  49526  ehl2eudis0lt  49534  rrx2linest  49550  line2x  49562  itsclc0yqsollem2  49571  seppsepf  49735  thincn0eu  50237  alseu-no-surprise  50644