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  4235  2reu4lem  4479  2reu4  4480  disjpr2  4674  ssunieq  4904  iuneq1  4968  iuneq2  4971  copsex2t  5469  propeqop  5484  opthhausdorff  5494  opthhausdorff0  5495  iunopeqop  5498  iunopeqopOLD  5499  soeq2  5585  opbrop  5753  xpsspw  5790  coeq1  5837  coeq2  5838  cnveq  5853  dmeq  5887  sotri  6121  tz7.7  6383  funun  6579  fununfun  6581  fundif  6582  funprg  6587  funtp  6590  2elresin  6653  funssxp  6731  fssres  6741  f1cof1  6783  foun  6836  f1un  6838  resdif  6839  f1oco  6841  fvun  6968  elfvmptrab1w  7014  elfvmptrab1  7015  fvn0ssdmfun  7067  dff3  7093  exfo  7098  fprg  7152  ftpg  7153  f1ounsn  7273  weisoeq2  7359  oprabv  7473  ndmovdistr  7603  ndmovord  7604  brrpssg  7726  eldifpw  7767  iunpw  7770  epweon  7774  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  8918  undifixp  8941  sbthlem8  9092  sbthlem9  9093  unxpdom  9229  isinf  9235  f1opwfi  9323  fiin  9392  en2lp  9585  inf3lem3  9609  brttrcl  9692  tcmin  9718  djuexb  9914  alephfp  10111  kmlem16  10168  endjudisj  10171  cofsmo  10271  fin23lem28  10342  axdc3lem2  10453  ac6c4  10483  brdom3  10531  brdom5  10532  brdom4  10533  canthp1lem2  10662  finngch  10664  ordpipq  10951  adderpq  10965  mulerpq  10966  lterpq  10979  genpn0  11012  genpnnp  11014  addclprlem2  11026  addcmpblnr  11078  addsrpr  11084  mulsrpr  11085  addclsr  11092  addasssr  11097  distrsr  11100  0idsr  11106  1idsr  11107  00sr  11108  mulgt0sr  11114  axaddf  11154  axaddass  11165  axdistr  11167  cnegex  11415  recextlem2  11869  difgtsumgt  12581  zaddcl  12658  qaddcl  13015  qmulcl  13017  qreccl  13019  xmulgt0  13335  xrsupsslem  13359  xrinfmsslem  13360  supxrpnf  13370  iccss  13467  difreicc  13537  fzadd2  13614  fzsubel  13615  ssfzunsnext  13624  difelfznle  13697  2ffzeq  13704  nelfzo  13720  fzonmapblen  13764  ubmelfzo  13786  ubmelm1fzo  13819  elfznelfzo  13829  subfzo0  13849  adddivflid  13879  modaddid  13971  modifeq2int  13997  modaddmodup  13998  addmodlteq  14010  fsuppmapnn0fiub  14055  mulexp  14165  mulexpz  14166  leexp1a  14239  faclbnd  14354  hashunx  14450  hashgt23el  14489  wrdeq  14601  ccatcl  14639  swrdnd  14724  swrdnd0  14727  swrdsbslen  14734  swrdspsleq  14735  pfxccat1  14771  swrdswrdlem  14773  pfxccatin12lem2a  14796  swrdccatin2  14798  pfxccatin12lem2  14800  pfxccatin12  14802  swrdccat  14804  reuccatpfxs1  14816  repswswrd  14855  repswccat  14857  cshwidxn  14880  cshweqdif2  14890  2cshwcshw  14896  cshwcshid  14898  cshwcsh2id  14899  f1oun2prg  14988  s2eq2s1eq  15007  s3eqs2s1eq  15009  s3sndisj  15040  s3iunsndisj  15041  sqabsadd  15369  sqabssub  15370  abs2dif  15420  rexanuz  15433  o1of2  15700  o1rlimmul  15706  fsum2dlem  15856  isumltss  15937  fprodser  16036  fprodeq0  16062  fprod2dlem  16067  dvdscmulr  16374  dvdsmulcr  16375  summodnegmod  16376  difmod0  16377  dvds2ln  16379  dvdsflip  16407  divalglem9  16491  gcdcllem3  16591  gcdaddmlem  16614  sqgcd  16652  lcmcllem  16686  lcmabs  16695  lcmgcdlem  16696  lcmgcd  16697  lcmgcdeq  16702  lcmftp  16726  lcmfunsnlem2lem1  16728  qredeq  16747  cncongr1  16757  cncongr2  16758  isprm7  16799  hashgcdlem  16879  dvdsprmpweqle  16978  difsqpwdvds  16979  prmgaplem4  17146  cshwsidrepsw  17185  setsfun0  17264  setsstruct2  17266  xpsfrnel2  17650  isfunc  17953  tsrss  18677  chnpof1  18718  rabsubmgmd  18806  resmgmhm2  18814  mndpfsupp  18874  ismhm0  18898  mhmismgmhm  18899  mndissubm  18915  resmndismnd  18916  resmhm2  18930  submefmnd  19004  sursubmefmnd  19005  injsubmefmnd  19006  grpissubg  19270  gimco  19395  symg2bas  19520  pgrpsubgsymg  19536  symgextf  19544  fvcosymgeq  19556  gsmsymgreqlem1  19557  symgfixf1  19564  efgrelexlema  19876  gsum2dlem1  20097  gsum2dlem2  20098  dvdsr  20503  isrnghmmul  20583  c0ghm  20602  rhmisrnghm  20622  rimco  20658  subrngpropd  20730  subrgpropd  20770  rnghmsubcsetclem2  20794  rngcinv  20799  rhmsubcsetclem2  20823  rhmsubcrngclem2  20829  ringcinv  20833  srhmsubc  20842  isdrng3lem2  20915  islmhm2  21222  unichnlidl  21425  cmprmidlmcl  21538  psgnghm  21793  psgndiflemB  21813  frlmbas3  21989  frlmphl  21994  islindf4  22051  ressmpladd  22244  ressmplmul  22245  mplind  22286  mpomatmul  22668  mavmul0g  22775  1marepvsma1  22805  mdetdiag  22821  matunitlindflem1  22901  matunitlindflem2  22902  slesolvec  22904  cramerimplem2  22909  cramerimplem3  22910  cramerimp  22911  mat2pmatlin  22960  m2pmfzgsumcl  22973  monmatcollpw  23004  pmatcollpw3lem  23008  pmatcollpwscmatlem1  23014  chpmat1dlem  23060  chfacfisf  23079  chfacfisfcpmat  23080  chfacfpmmulgsum2  23090  tgcl  23194  uncld  23266  innei  23350  cnco  23491  uncmp  23628  txbas  23793  txbasval  23832  tx1stc  23876  fbun  24066  infil  24089  fbunfip  24095  filuni  24111  imaelfm  24177  txflf  24232  tsmsfbas  24354  tsmsxp  24381  blin2  24655  nmhmplusg  24983  qtopbaslem  24984  iccntr  25048  ncvspi  25384  ncvs1  25385  unmbl  25765  volfiniun  25775  mbfi1flimlem  25950  ply1idom  26350  logreclem  26999  relogbcxpb  27024  fsumvma2  27450  chpchtsum  27455  dchrelbas3  27474  dchrmulcl  27485  lgsmulsqcoprm  27579  gausslemma2dlem1a  27601  lgsquad2lem2  27621  dchrisum0fmul  27742  dchrisum0lem1  27752  ltsres  27898  nocvxminlem  28019  oldlim  28152  madebdayim  28153  madebdaylemlrcut  28164  readdscl  28764  remulscl  28767  ishpg  29116  brcgr  29357  brbtwn2  29362  axcontlem2  29422  uspgredg2v  29684  usgredg2v  29687  usgr2v1e2w  29712  nb3gr2nb  29844  cusgredg  29884  cplgr3v  29895  cusgrop  29898  rusgr1vtx  30048  iswlkg  30073  wlkeq  30093  wlk1walk  30098  uspgr2wlkeq2  30106  uspgr2wlkeqi  30107  cyclnumvtx  30267  crctcshwlkn0lem3  30280  crctcshwlkn0lem4  30281  crctcshwlkn0lem5  30282  wspthneq1eq2  30328  wwlksnextinj  30367  2wlkdlem7  30400  2wlkdlem8  30401  2pthon3v  30411  s3wwlks2on  30424  sps3wwlks2on  30425  elwwlks2  30437  elwspths2spth  30438  rusgrnumwwlks  30445  clwlkclwwlklem2a  30468  clwlkclwwlklem3  30471  clwlkclwwlkf1lem2  30475  clwlkclwwlkf1  30480  clwwlknonex2  30579  3wlkdlem3  30641  uhgr3cyclex  30662  cusconngr  30671  eupth0  30694  frgr3v  30755  1to3vfriswmgr  30760  4cycl2v2nb  30769  frgrnbnb  30773  frgrncvvdeq  30789  frgrwopreglem4a  30790  frgrwopreglem5a  30791  frgrwopreglem4  30795  frgrwopreglem5  30801  frgrhash2wsp  30812  numclwwlk1lem2foa  30834  numclwwlk2  30861  blocni  31286  hvsub4  31518  shscli  31798  shscom  31800  spanunsni  32060  spanpr  32061  5oalem2  32136  5oalem3  32137  5oalem5  32139  3oalem1  32143  hoscl  32226  hoadddi  32284  hoadddir  32285  hosub4  32294  lnophsi  32482  hmops  32501  hmopm  32502  adjadd  32574  leop2  32605  leopadd  32613  leopmuli  32614  pjclem4  32680  pj3si  32688  mdslmd1lem2  32807  mdslmd3i  32813  atomli  32863  atcvatlem  32866  chirredlem3  32873  chirredi  32875  atcvat3i  32877  mdsymlem1  32884  mdsymlem5  32888  cdjreui  32913  cdj3i  32922  addltmulALT  32927  hashxpe  33278  domnmuln0rd  33717  mndpluscn  34436  sxbrsigalem5  34799  probfinmeasbALTV  34940  bnj545  35404  bnj546  35405  bnj557  35410  bnj570  35414  bnj594  35421  bnj1001  35468  bnj1118  35493  txpconn  35811  cvmlift2lem10  35891  gonar  35974  lediv2aALT  36256  altopeq12  36542  altxpsspw  36557  funtransport  36611  neibastop1  36978  filnetlem3  36999  lukshef-ax2  37034  arg-ax  37035  nndivsub  37076  bj-nnfan  37487  bj-nnfor  37489  cgsex2gd  37889  copsex2b  37892  isbasisrelowllem1  38109  isbasisrelowllem2  38110  icoreclin  38111  relowlssretop  38117  rdgeqoa  38124  fvineqsnf1  38164  poimirlem4  38373  poimirlem26  38395  poimirlem29  38398  poimirlem30  38399  heicant  38404  mblfinlem1  38406  ismblfin  38410  itg2addnclem  38420  ftc1anclem6  38447  ftc1anclem7  38448  ftc1anclem8  38449  ftc1anc  38450  prdstotbnd  38544  heibor1lem  38559  isdrngo2  38708  divrngidl  38778  pridlc3  38823  eldisjdmqsim  39565  linepsubN  40625  pmapsub  40641  elpaddri  40675  paddasslem14  40706  pmapjoin  40725  dvhfvadd  41964  dvhvaddcomN  41969  bcle2d  43045  imacrhmcl  43402  rmxynorm  43759  monotoddzzfi  43783  acongtr  43819  mpaaeu  43991  oaltublim  44131  omord2lim  44141  cantnftermord  44161  dflim5  44170  omabs2  44173  tfsconcat0i  44186  ofoafo  44197  naddcnff  44203  oaun3lem1  44215  oaun3lem2  44216  pr2cv  44388  brfvrcld2  44532  rfovcnvf1od  44844  ismnushort  45125  nzin  45142  pm10.14  45183  disjrnmpt2  46020  liminfvalxr  46611  etransclem38  47100  wrddin  47714  cfsetsnfsetf1  47947  tz6.12-afv2  48128  2elfz2melfz  48206  fz0addge0  48207  2ffzoeq  48216  difltmodne  48236  modn0mul  48251  mod2addne  48258  icceuelpartlem  48335  icceuelpart  48336  ich2exprop  48371  sqrtpwpw2p  48441  fmtnoprmfac1lem  48467  fmtnoprmfac1  48468  lighneallem2  48509  divgcdoddALTV  48598  gbowpos  48675  gbowgt5  48678  gboge9  48680  nnsum3primesgbe  48708  bgoldbtbndlem2  48722  bgoldbtbndlem3  48723  isuspgrim  48812  clnbgrgrimlem  48849  clnbgrgrim  48850  isgrtri  48859  isubgr3stgrlem4  48885  grlimgrtri  48919  grlictr  48931  gpgedgvtx0  48977  gpgedg2iv  48983  gpg5nbgrvtx03star  48996  gpg5nbgr3star  48997  pgnbgreunbgrlem3  49034  pgnbgreunbgrlem6  49040  pgn4cyclex  49042  isupwlkg  49053  rngcinvALTV  49191  ringcinvALTV  49225  srhmsubcALTV  49240  mapprop  49276  zlmodzxzadd  49288  domnmsuppn0  49299  ply1mulgsumlem2  49317  lincsum  49359  lincsumcl  49361  lincscmcl  49362  isldepslvec2  49415  digexp  49537  rrx2pnecoorneor  49645  rrx2pnedifcoorneorr  49647  rrx2xpref1o  49648  ehl2eudis0lt  49656  rrx2linest  49672  line2x  49684  itsclc0yqsollem2  49693  seppsepf  49855  thincn0eu  50357  alseu-no-surprise  50767