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

Syntax hints:   → wi 4   ∧ wa 400

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 210  df-an 401

This theorem is referenced by:  anim12ci  625  anim1i  626  anim2i  628  anifp  1088  cgsex2g  3500  cgsex4g  3501  spc2egv  3559  spc2ed  3561  uneqin  4243  2reu4lem  4485  2reu4  4486  disjpr2  4680  ssunieq  4910  iuneq1  4974  iuneq2  4977  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  6388  funun  6584  fununfun  6586  fundif  6587  funprg  6592  funtp  6595  2elresin  6658  funssxp  6736  fssres  6746  f1cof1  6788  foun  6841  f1un  6843  resdif  6844  f1oco  6846  fvun  6973  elfvmptrab1w  7019  elfvmptrab1  7020  fvn0ssdmfun  7071  dff3  7097  exfo  7102  fprg  7154  ftpg  7155  f1ounsn  7272  weisoeq2  7356  oprabv  7472  ndmovdistr  7601  ndmovord  7602  brrpssg  7724  eldifpw  7768  iunpw  7771  epweon  7775  bropfvvvv  8088  f1o2ndf1  8118  poseq  8155  fvn0elsupp  8177  smores  8340  tz7.49  8433  tz7.49c  8434  oaord  8533  oeeulem  8588  nnaord  8606  brecop  8809  brecop2  8810  eroveu  8811  ecopovtrn  8819  ixpeq2  8910  undifixp  8933  sbthlem8  9083  sbthlem9  9084  unxpdom  9220  isinf  9226  f1opwfi  9314  fiin  9383  en2lp  9576  inf3lem3  9600  brttrcl  9683  tcmin  9709  djuexb  9896  alephfp  10093  kmlem16  10150  endjudisj  10153  cofsmo  10254  fin23lem28  10325  axdc3lem2  10436  ac6c4  10466  brdom3  10513  brdom5  10514  brdom4  10515  canthp1lem2  10639  finngch  10641  ordpipq  10928  adderpq  10942  mulerpq  10943  lterpq  10956  genpn0  10989  genpnnp  10991  addclprlem2  11003  addcmpblnr  11055  addsrpr  11061  mulsrpr  11062  addclsr  11069  addasssr  11074  distrsr  11077  0idsr  11083  1idsr  11084  00sr  11085  mulgt0sr  11091  axaddf  11131  axaddass  11142  axdistr  11144  cnegex  11392  recextlem2  11846  difgtsumgt  12558  zaddcl  12635  qaddcl  12990  qmulcl  12992  qreccl  12994  xmulgt0  13310  xrsupsslem  13334  xrinfmsslem  13335  supxrpnf  13345  iccss  13442  difreicc  13512  fzadd2  13589  fzsubel  13590  ssfzunsnext  13599  difelfznle  13672  2ffzeq  13679  nelfzo  13695  fzonmapblen  13739  ubmelfzo  13761  ubmelm1fzo  13794  elfznelfzo  13804  subfzo0  13823  adddivflid  13853  modaddid  13945  modifeq2int  13971  modaddmodup  13972  addmodlteq  13984  fsuppmapnn0fiub  14029  mulexp  14139  mulexpz  14140  leexp1a  14213  faclbnd  14328  hashunx  14424  hashgt23el  14463  wrdeq  14575  ccatcl  14613  swrdnd  14694  swrdnd0  14697  swrdsbslen  14704  swrdspsleq  14705  pfxccat1  14741  swrdswrdlem  14743  pfxccatin12lem2a  14766  swrdccatin2  14768  pfxccatin12lem2  14770  pfxccatin12  14772  swrdccat  14774  reuccatpfxs1  14786  repswswrd  14823  repswccat  14825  cshwidxn  14848  cshweqdif2  14858  2cshwcshw  14864  cshwcshid  14866  cshwcsh2id  14867  f1oun2prg  14956  s2eq2s1eq  14975  s3eqs2s1eq  14977  s3sndisj  15006  s3iunsndisj  15007  sqabsadd  15335  sqabssub  15336  abs2dif  15386  rexanuz  15399  o1of2  15666  o1rlimmul  15672  fsum2dlem  15823  isumltss  15904  fprodser  16005  fprodeq0  16031  fprod2dlem  16036  dvdscmulr  16343  dvdsmulcr  16344  summodnegmod  16345  difmod0  16346  dvds2ln  16348  dvdsflip  16376  divalglem9  16460  gcdcllem3  16560  gcdaddmlem  16583  sqgcd  16621  lcmcllem  16655  lcmabs  16664  lcmgcdlem  16665  lcmgcd  16666  lcmgcdeq  16671  lcmftp  16695  lcmfunsnlem2lem1  16697  qredeq  16716  cncongr1  16726  cncongr2  16727  isprm7  16768  hashgcdlem  16848  dvdsprmpweqle  16947  difsqpwdvds  16948  prmgaplem4  17115  cshwsidrepsw  17154  setsfun0  17233  setsstruct2  17235  xpsfrnel2  17619  isfunc  17922  tsrss  18646  chnpof1  18687  rabsubmgmd  18763  resmgmhm2  18771  mndpfsupp  18826  ismhm0  18849  mhmismgmhm  18850  mndissubm  18866  resmndismnd  18867  resmhm2  18881  submefmnd  18955  sursubmefmnd  18956  injsubmefmnd  18957  grpissubg  19214  gimco  19339  symg2bas  19464  pgrpsubgsymg  19480  symgextf  19488  fvcosymgeq  19500  gsmsymgreqlem1  19501  symgfixf1  19508  efgrelexlema  19820  gsum2dlem1  20041  gsum2dlem2  20042  dvdsr  20445  isrnghmmul  20525  c0ghm  20544  rhmisrnghm  20563  subrngpropd  20654  subrgpropd  20694  rnghmsubcsetclem2  20718  rngcinv  20723  rhmsubcsetclem2  20747  rhmsubcrngclem2  20753  ringcinv  20757  srhmsubc  20766  islmhm2  21140  unichnlidl  21343  cmprmidlmcl  21456  psgnghm  21711  psgndiflemB  21731  frlmbas3  21907  frlmphl  21912  islindf4  21969  ressmpladd  22160  ressmplmul  22161  mplind  22202  mpomatmul  22584  mavmul0g  22691  1marepvsma1  22721  mdetdiag  22737  slesolvec  22817  cramerimplem2  22822  cramerimplem3  22823  cramerimp  22824  mat2pmatlin  22873  m2pmfzgsumcl  22886  monmatcollpw  22917  pmatcollpw3lem  22921  pmatcollpwscmatlem1  22927  chpmat1dlem  22973  chfacfisf  22992  chfacfisfcpmat  22993  chfacfpmmulgsum2  23003  tgcl  23107  uncld  23179  innei  23263  cnco  23404  uncmp  23541  txbas  23705  txbasval  23744  tx1stc  23788  fbun  23978  infil  24001  fbunfip  24007  filuni  24023  imaelfm  24089  txflf  24144  tsmsfbas  24266  tsmsxp  24293  blin2  24567  nmhmplusg  24895  qtopbaslem  24896  iccntr  24960  ncvspi  25296  ncvs1  25297  unmbl  25677  volfiniun  25687  mbfi1flimlem  25862  ply1idom  26263  logreclem  26908  relogbcxpb  26933  fsumvma2  27359  chpchtsum  27364  dchrelbas3  27383  dchrmulcl  27394  lgsmulsqcoprm  27488  gausslemma2dlem1a  27510  lgsquad2lem2  27530  dchrisum0fmul  27651  dchrisum0lem1  27661  ltsres  27807  nocvxminlem  27928  oldlim  28061  madebdayim  28062  madebdaylemlrcut  28073  readdscl  28673  remulscl  28676  ishpg  29022  brcgr  29231  brbtwn2  29236  axcontlem2  29296  uspgredg2v  29555  usgredg2v  29558  usgr2v1e2w  29583  nb3gr2nb  29715  cusgredg  29755  cplgr3v  29766  cusgrop  29769  rusgr1vtx  29919  iswlkg  29944  wlkeq  29964  wlk1walk  29969  uspgr2wlkeq2  29977  uspgr2wlkeqi  29978  cyclnumvtx  30130  crctcshwlkn0lem3  30142  crctcshwlkn0lem4  30143  crctcshwlkn0lem5  30144  wspthneq1eq2  30190  wwlksnextinj  30229  2wlkdlem7  30262  2wlkdlem8  30263  2pthon3v  30273  s3wwlks2on  30286  sps3wwlks2on  30287  elwwlks2  30299  elwspths2spth  30300  rusgrnumwwlks  30307  clwlkclwwlklem2a  30330  clwlkclwwlklem3  30333  clwlkclwwlkf1lem2  30337  clwlkclwwlkf1  30342  clwwlknonex2  30441  3wlkdlem3  30493  uhgr3cyclex  30514  cusconngr  30523  eupth0  30546  frgr3v  30607  1to3vfriswmgr  30612  4cycl2v2nb  30621  frgrnbnb  30625  frgrncvvdeq  30641  frgrwopreglem4a  30642  frgrwopreglem5a  30643  frgrwopreglem4  30647  frgrwopreglem5  30653  frgrhash2wsp  30664  numclwwlk1lem2foa  30686  numclwwlk2  30713  blocni  31138  hvsub4  31370  shscli  31650  shscom  31652  spanunsni  31912  spanpr  31913  5oalem2  31988  5oalem3  31989  5oalem5  31991  3oalem1  31995  hoscl  32078  hoadddi  32136  hoadddir  32137  hosub4  32146  lnophsi  32334  hmops  32353  hmopm  32354  adjadd  32426  leop2  32457  leopadd  32465  leopmuli  32466  pjclem4  32532  pj3si  32540  mdslmd1lem2  32659  mdslmd3i  32665  atomli  32715  atcvatlem  32718  chirredlem3  32725  chirredi  32727  atcvat3i  32729  mdsymlem1  32736  mdsymlem5  32740  cdjreui  32765  cdj3i  32774  addltmulALT  32779  hashxpe  33133  domnmuln0rd  33578  mndpluscn  34297  sxbrsigalem5  34659  probfinmeasbALTV  34800  bnj545  35264  bnj546  35265  bnj557  35270  bnj570  35274  bnj594  35281  bnj1001  35328  bnj1118  35353  txpconn  35705  cvmlift2lem10  35785  gonar  35868  lediv2aALT  36150  altopeq12  36435  altxpsspw  36450  funtransport  36504  neibastop1  36851  filnetlem3  36872  lukshef-ax2  36907  arg-ax  36908  nndivsub  36949  bj-nnfan  37360  bj-nnfor  37362  cgsex2gd  37762  copsex2b  37765  isbasisrelowllem1  37982  isbasisrelowllem2  37983  icoreclin  37984  relowlssretop  37990  rdgeqoa  37997  fvineqsnf1  38037  matunitlindflem1  38248  matunitlindflem2  38249  poimirlem4  38256  poimirlem26  38278  poimirlem29  38281  poimirlem30  38282  heicant  38287  mblfinlem1  38289  ismblfin  38293  itg2addnclem  38303  ftc1anclem6  38330  ftc1anclem7  38331  ftc1anclem8  38332  ftc1anc  38333  prdstotbnd  38426  heibor1lem  38441  isdrngo2  38590  divrngidl  38660  pridlc3  38705  eldisjdmqsim  39447  linepsubN  40507  pmapsub  40523  elpaddri  40557  paddasslem14  40588  pmapjoin  40607  dvhfvadd  41846  dvhvaddcomN  41851  bcle2d  42927  imacrhmcl  43269  rimco  43270  rmxynorm  43628  monotoddzzfi  43652  acongtr  43688  mpaaeu  43860  oaltublim  44000  omord2lim  44010  cantnftermord  44030  dflim5  44039  omabs2  44042  tfsconcat0i  44055  ofoafo  44066  naddcnff  44072  oaun3lem1  44084  oaun3lem2  44085  pr2cv  44257  brfvrcld2  44401  rfovcnvf1od  44713  ismnushort  44994  nzin  45011  pm10.14  45052  disjrnmpt2  45889  liminfvalxr  46480  etransclem38  46969  cfsetsnfsetf1  47779  tz6.12-afv2  47960  2elfz2melfz  48038  fz0addge0  48039  2ffzoeq  48048  difltmodne  48068  modn0mul  48083  mod2addne  48090  icceuelpartlem  48167  icceuelpart  48168  ich2exprop  48203  sqrtpwpw2p  48273  fmtnoprmfac1lem  48299  fmtnoprmfac1  48300  lighneallem2  48341  divgcdoddALTV  48430  gbowpos  48507  gbowgt5  48510  gboge9  48512  nnsum3primesgbe  48540  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  isuspgrim  48644  clnbgrgrimlem  48681  clnbgrgrim  48682  isgrtri  48691  isubgr3stgrlem4  48717  grlimgrtri  48751  grlictr  48763  gpgedgvtx0  48809  gpgedg2iv  48815  gpg5nbgrvtx03star  48828  gpg5nbgr3star  48829  pgnbgreunbgrlem3  48866  pgnbgreunbgrlem6  48872  pgn4cyclex  48874  isupwlkg  48885  rngcinvALTV  49024  ringcinvALTV  49058  srhmsubcALTV  49073  mapprop  49109  zlmodzxzadd  49121  domnmsuppn0  49132  ply1mulgsumlem2  49150  lincsum  49192  lincsumcl  49194  lincscmcl  49195  isldepslvec2  49248  digexp  49370  rrx2pnecoorneor  49478  rrx2pnedifcoorneorr  49480  rrx2xpref1o  49481  ehl2eudis0lt  49489  rrx2linest  49505  line2x  49517  itsclc0yqsollem2  49526  seppsepf  49690  thincn0eu  50192